Adapt to coq/coq#18938 (EConstr.ERelevance)

damien-pous · Apr 23, 2024 · dbb5713 · dbb5713
1 parent a5c88eb
commit dbb5713
Show file tree

Hide file tree

Showing 4 changed files with 8 additions and 8 deletions.
diff --git a/src/common.ml b/src/common.ml
@@ -46,7 +46,7 @@ let convertible' (env,sigma) = Reductionops.is_conv env sigma
 (* creating a name and a reference to that name *)
 let fresh_name env n =
   let vname = Tactics.fresh_id_in_env Id.Set.empty (Id.of_string n) env in
-    Context.annotR vname, mkVar vname
+    annotR vname, mkVar vname
 
 (* access to Coq constants *)
 let get_const dir s = 

diff --git a/src/common.mli b/src/common.mli
@@ -7,12 +7,12 @@ val tc_find :
 val new_evar :
   Environ.env -> Evd.evar_map -> EConstr.types -> Evd.evar_map * EConstr.t
 val push :
-  Names.Name.t Context.binder_annot ->
+  Names.Name.t EConstr.binder_annot ->
   EConstr.types -> Environ.env -> Environ.env
 val convertible :
   Environ.env -> Evd.evar_map -> EConstr.constr -> EConstr.constr -> bool
 val fresh_name :
-  Environ.env -> string -> Names.Id.t Context.binder_annot * EConstr.t
+  Environ.env -> string -> Names.Id.t EConstr.binder_annot * EConstr.t
 val get_const : string list -> string -> EConstr.t lazy_t
 val force_app : EConstr.t Lazy.t -> EConstr.t array -> EConstr.t
 val partial_app : int -> EConstr.t -> EConstr.t array -> EConstr.t

diff --git a/src/kat_reification.ml b/src/kat_reification.ml
@@ -78,8 +78,8 @@ end = struct
 	t := (x,y,z)::l; 1+List.length l
 
   let to_env t typ def = match !t with
-    | [] -> mkLambda (Context.anonR,Lazy.force Pos.t,def)
-    | [_,x,_] -> mkLambda (Context.anonR,Lazy.force Pos.t,x)
+    | [] -> mkLambda (anonR,Lazy.force Pos.t,def)
+    | [_,x,_] -> mkLambda (anonR,Lazy.force Pos.t,x)
     | (_,x,_)::q ->
 	Pos.sigma_get typ x
 	  (snd (List.fold_left
@@ -366,7 +366,7 @@ let reify_kat_goal ?kat check =
     mkNamedLetIn sigma tenv_n tenv (mkArrowR (Lazy.force Pos.t) typ) (
     mkNamedLetIn sigma env_n env (mkArrowR (Lazy.force Pos.t) pck) (
     mkNamedLetIn sigma penv_n penv 
-      (mkProd (Context.anonR,Lazy.force Pos.t,
+      (mkProd (anonR,Lazy.force Pos.t,
                mkArrowR (Lazy.force Pos.t)
   		 (Lattice.car (lops (mkApp (tenv_ref,[|mkRel 2|])))))) (
     mkNamedLetIn sigma src_n src_v (mkArrowR (Lazy.force Pack.var) (Lazy.force Pos.t)) (

diff --git a/src/reification.ml b/src/reification.ml
@@ -51,8 +51,8 @@ end = struct
 	  t := ((x,j,y)::l,i+1); j
 
   let to_env t typ def = match fst !t with
-    | [] -> mkLambda (Context.anonR,Lazy.force Pos.t,def)
-    | [_,_,x] -> mkLambda (Context.anonR,Lazy.force Pos.t,x)
+    | [] -> mkLambda (anonR,Lazy.force Pos.t,def)
+    | [_,_,x] -> mkLambda (anonR,Lazy.force Pos.t,x)
     | (_,_,x)::q ->
 	Pos.sigma_get typ x
 	  (List.fold_left