Merge pull request #1080 from SkySkimmer/erelevance

Adapt to coq/coq#18938 (EConstr.ERelevance)
MetaCoq · Apr 23, 2024 · e27b549 · e27b549
2 parents d8c5fe0 + 755a982
commit e27b549
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 7 deletions.
diff --git a/template-coq/src/ast_denoter.ml b/template-coq/src/ast_denoter.ml
@@ -143,7 +143,7 @@ struct
     | Coq_nAnon -> Anonymous
     | Coq_nNamed n -> Name (unquote_ident n)
 
-  let unquote_aname (q: quoted_aname) : Name.t Context.binder_annot =
+  let unquote_aname (q: quoted_aname) : Name.t Constr.binder_annot =
     {Context.binder_name = unquote_name q.binder_name;
      Context.binder_relevance = unquote_relevance q.binder_relevance}
 

diff --git a/template-coq/src/denoter.ml b/template-coq/src/denoter.ml
@@ -8,7 +8,7 @@ sig
 
   val unquote_ident : quoted_ident -> Id.t
   val unquote_name : quoted_name -> Name.t
-  val unquote_aname : quoted_aname -> Name.t Context.binder_annot
+  val unquote_aname : quoted_aname -> Name.t Constr.binder_annot
   val unquote_relevance : quoted_relevance -> Sorts.relevance
   val unquote_evar : Environ.env -> Evd.evar_map -> quoted_int -> Constr.t list -> Evd.evar_map * Constr.t
   val unquote_int : quoted_int -> int

diff --git a/template-coq/src/quoter.ml b/template-coq/src/quoter.ml
@@ -38,7 +38,7 @@ let warn_ignoring_private_polymorphic_universes =
   CWarnings.create_in (make_warning_if_not_exist "private-polymorphic-universes-ignored")
           Pp.(fun () -> str "Ignoring private polymorphic universes.")
 
-let toDecl (old: Name.t Context.binder_annot * ((Constr.constr) option) * Constr.constr) : Constr.rel_declaration =
+let toDecl (old: Name.t Constr.binder_annot * ((Constr.constr) option) * Constr.constr) : Constr.rel_declaration =
   let (name,value,typ) = old in
   match value with
   | Some value -> Context.Rel.Declaration.LocalDef (name,value,typ)
@@ -93,7 +93,7 @@ sig
 
   val quote_ident : Id.t -> quoted_ident
   val quote_name : Name.t -> quoted_name
-  val quote_aname : Name.t Context.binder_annot -> quoted_aname
+  val quote_aname : Name.t Constr.binder_annot -> quoted_aname
   val quote_relevance : Sorts.relevance -> quoted_relevance
   val quote_int : int -> quoted_int
   val quote_bool : bool -> quoted_bool

diff --git a/template-coq/src/tm_util.ml b/template-coq/src/tm_util.ml
@@ -216,13 +216,14 @@ module RetypeMindEntry =
     Typing.type_of env evm (EConstr.of_constr c)
 
   let retype_decl env evm decl =
+    let decl = EConstr.of_rel_decl decl in
     match decl with
     | Context.Rel.Declaration.LocalAssum (na, ty) ->
-      let evm, ty = Typing.solve_evars env evm (EConstr.of_constr ty) in
+      let evm, ty = Typing.solve_evars env evm ty in
       evm, Context.Rel.Declaration.LocalAssum (na, ty)
     | Context.Rel.Declaration.LocalDef (na, b, ty) ->
-      let evm, b = Typing.solve_evars env evm (EConstr.of_constr b) in
-      let evm, ty = Typing.solve_evars env evm (EConstr.of_constr ty) in
+      let evm, b = Typing.solve_evars env evm b in
+      let evm, ty = Typing.solve_evars env evm ty in
       let evm = Typing.check env evm b ty in
       evm, Context.Rel.Declaration.LocalDef (na, b, ty)