Hello again,

I'm meeting a problem while unquoting something that I've just quoted that may be a bug.

I'm using coq.8.11.0 on Vscoq.

```
Definition mkImpl (A B : term) : term := (* comes from demo.v in the repo*)
tProd nAnon A B.
Quote Definition reif_forallP_P_implies_P := Eval compute in (forall (P:Prop), P ->P ).
Make Definition uq_reif_forallP_implies_P := reif_forallP_P_implies_P.
```

The Make Definition outputs the following error:

```
The term "forall P : Prop, P -> P" has type "Type" while it is expected to have type "Prop".
```

Likewise, when I try to build the reification of `forall (P : Prop), P -> P.`

:

```
Quote Definition reif_Prop := Eval compute in Prop.
Definition reif_forallP_P_implies_P' := tProd nAnon reif_Type_Term (mkImpl (tRel 0) (tRel 0)).
Make Definition uq_reif_forallP_implies_P' := trad_works_Prop.
```

This time, the Make Definition raises the following (different) error:

```
Anomaly "Not a sort." Please report at http://coq.inria.fr/bugs/.
Not in proof mode.
```

When I print reif_Prop, I obtain,

```
reif_Prop = tSort (Universe.make'' (Level.lProp, false) [])
: term
```

So, what is wrong and how should I unquote (the reification of) `forall (P : Prop), P -> P.`

?

In `reif_forallP_P_implies_P'`

shouldn't you use `tProd nAnon reif_Prop`

instead of `tProd nAnon reif_Type_Term`

?

Huh, yes, sorry, here is the right code:

```
Definition reif_forallP_P_implies_P' := tProd nAnon reif_Prop (mkImpl (tRel 0) (tRel 0)).
Make Definition uq_reif_forallP_implies_P' := reif_forallP_P_implies_P'.
```

but I still get the same error message

@Matthieu Sozeau can you confirm this is a bug?

Wait can you try with just

```
From MetaCoq Require Import All.
Quote Definition reif_forallP_P_implies_P := Eval compute in (forall (P:Prop), P ->P ).
Make Definition uq_reif_forallP_implies_P := reif_forallP_P_implies_P.
```

For me it works with no errors.

I just did. I still get:

```
The term "forall P : Prop, P -> P" has type "Type" while it is expected to have type "Prop".
Not in proof mode.
```

but perhaps it is related to opam installation then?

That's pretty weird…

Maybe try in a new file? There may be something weird in the context?

I did it at the very beginning of a new file, but the error was the same :/

Théo Winterhalter said:

Matthieu Sozeau can you confirm this is a bug?

It looks like one

Maybe we're not talking about the same version of MetaCoq though, if it works for Théo. @Pierre Vial what does your `opam list`

say?

It gives me this:

```
base-bigarray base
base-threads base
base-unix base
camlp5 7.11 Preprocessor-pretty-printer of OCaml
conf-findutils 1 Virtual package relying on findutils
conf-m4 1 Virtual package relying on m4
coq 8.9.1 Formal proof management system
coq-equations 1.2.1+8.9 A function definition package for Coq
coq-metacoq 1.0~alpha+8.9 A meta-programming framework for Coq
coq-metacoq-checker 1.0~alpha+8.9 Specification of Coq's type theory and re
coq-metacoq-erasure 1.0~alpha+8.9 Implementation and verification of an era
coq-metacoq-pcuic 1.0~alpha+8.9 A type system equivalent to Coq's and its
coq-metacoq-safechecker 1.0~alpha+8.9 Implementation and verification of safe c
coq-metacoq-template 1.0~alpha+8.9 A quoting and unquoting library for Coq i
coq-metacoq-translations 1.0~alpha+8.9 Implementation and verification of an era
num 1.3 The legacy Num library for arbitrary-prec
ocaml 4.09.0 The OCaml compiler (virtual package)
ocaml-base-compiler 4.09.0 Official release 4.09.0
ocaml-config 1 OCaml Switch Configuration
ocamlfind 1.8.1 A library manager for OCaml
```

I'm a bit surprised, because opam switch tells me that I'm using my coq.8.11.0 switch

Hmm, yep it looks like you coq.8.11.0 switch has coq 8.9. So you might be seeing a bug in an old version of metacoq

Ok thanks ! I'll try to install it again

Last updated: Feb 09 2023 at 03:06 UTC