Merge pull request #43 from SkySkimmer/erelevance

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

src/reify.ml

@@ -10,7 +10,7 @@ open Constr
 open EConstr
 open Names
 
-let mkArrow x y = mkArrow x Sorts.Relevant y
+let mkArrow x y = mkArrow x ERelevance.relevant y
 
 (* pick an element in an hashtbl *)
 let hashtbl_pick t = Hashtbl.fold (fun i x -> function None -> Some (i,x) | acc -> acc) t None
@@ -215,8 +215,8 @@ end = struct
 	  t := ((x,j,Lazy.force y)::l,i+1); j
 
   let to_env t typ def = match fst !t with
-    | [] -> mkLambda (Context.make_annot Anonymous Sorts.Relevant,Lazy.force Coq.positive,def)
-    | [_,_,x] -> mkLambda (Context.make_annot Anonymous Sorts.Relevant,Lazy.force Coq.positive,x)
+    | [] -> mkLambda (Context.make_annot Anonymous ERelevance.relevant,Lazy.force Coq.positive,def)
+    | [_,_,x] -> mkLambda (Context.make_annot Anonymous ERelevance.relevant,Lazy.force Coq.positive,x)
     | (_,_,x)::q ->
 	Reification.sigma_get typ x
 	  (List.fold_left
@@ -335,10 +335,10 @@ let reify_goal ops =
 
 	(* reified goal conclusion: add the relation over the two evaluated members *)
 	let reified = 
-	  mkNamedLetIn sigma (Context.make_annot tenv_name Sorts.Relevant) tenv (mkArrow (Lazy.force Coq.positive) typ) (
-	    mkNamedLetIn sigma (Context.make_annot env_name Sorts.Relevant) tenv' (Reification.env_type gph) (
-	      mkNamedLetIn sigma (Context.make_annot ln Sorts.Relevant) lv x (
-		mkNamedLetIn sigma (Context.make_annot rn Sorts.Relevant) rv x (
+          mkNamedLetIn sigma (Context.make_annot tenv_name ERelevance.relevant) tenv (mkArrow (Lazy.force Coq.positive) typ) (
+            mkNamedLetIn sigma (Context.make_annot env_name ERelevance.relevant) tenv' (Reification.env_type gph) (
+              mkNamedLetIn sigma (Context.make_annot ln ERelevance.relevant) lv x (
+                mkNamedLetIn sigma (Context.make_annot rn ERelevance.relevant) rv x (
 		  (mkApp (rel, [|Reification.typ gph env_ref src; Reification.typ gph env_ref tgt;l;r|]))))))
 	in
 	  (try