Merge PR #8817: SProp: the definitionally proof irrelevant universe

Ack-by: JasonGross
Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Reviewed-by: ejgallego
Ack-by: gares
Ack-by: mattam82

3 files changed, 7 insertions, 7 deletions

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 286021d68e..1c9ab2e3bd 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -107,7 +107,7 @@ let mk_open_instance env evmap id idc m t =
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
       let (nam,_,_)=destProd evmap (whd_all env evmap typ) in
-	match nam with
+        match nam.Context.binder_name with
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
   let revt=substl (List.init m (fun i->mkRel (m-i))) t in
@@ -115,7 +115,7 @@ let mk_open_instance env evmap id idc m t =
     if Int.equal n 0 then evmap, decls else
       let nid=(fresh_id_in_env avoid var_id env) in
       let (evmap, (c, _)) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
-      let decl = LocalAssum (Name nid, c) in
+      let decl = LocalAssum (Context.make_annot (Name nid) Sorts.Relevant, c) in
 	aux (n-1) (Id.Set.add nid avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
   let evmap, decls = aux m Id.Set.empty env evmap [] in
   (evmap, decls, revt)
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 832a98b7f8..7f06ab6777 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -163,9 +163,9 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq =
 let ll_arrow_tac a b c backtrack id continue seq=
   let open EConstr in
   let open Vars in
-  let cc=mkProd(Anonymous,a,(lift 1 b)) in
-  let d idc = mkLambda (Anonymous,b,
-		  mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
+  let cc=mkProd(Context.make_annot Anonymous Sorts.Relevant,a,(lift 1 b)) in
+  let d idc = mkLambda (Context.make_annot Anonymous Sorts.Relevant,b,
+                  mkApp (idc, [|mkLambda (Context.make_annot Anonymous Sorts.Relevant,(lift 1 a),(mkRel 2))|])) in
     tclORELSE
       (tclTHENS (cut c)
 	 [tclTHENLIST
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index d63fe9d799..0c958ddee3 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -65,13 +65,13 @@ let unif evd t1 t2=
 		    bind i t else raise (UFAIL(nt1,nt2))
 	  | Cast(_,_,_),_->Queue.add (strip_outer_cast evd nt1,nt2) bige
  	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast evd nt2) bige
-	  | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
+          | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
 	      Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
 	  | Case (_,pa,ca,va),Case (_,pb,cb,vb)->
 	      Queue.add (pa,pb) bige;
 	      Queue.add (ca,cb) bige;
 	      let l=Array.length va in
-		if not (Int.equal l (Array.length vb)) then
+                if not (Int.equal l (Array.length vb)) then
 		  raise (UFAIL (nt1,nt2))
 		else
 		  for i=0 to l-1 do