From 5143129baac805d3a49ac3ee9f3344c7a447634f Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 30 Oct 2016 17:53:07 +0100
Subject: Termops API using EConstr.

---
 plugins/firstorder/formula.ml | 12 ++++++------
 plugins/firstorder/rules.ml   |  4 ++--
 plugins/firstorder/unify.ml   | 13 ++++++++-----
 3 files changed, 16 insertions(+), 13 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index b34a364920..79f185d187 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -79,13 +79,13 @@ type kind_of_formula=
 let kind_of_formula gl term =
   let normalize=special_nf gl in
   let cciterm=special_whd gl term in
-    match match_with_imp_term cciterm with
-	Some (a,b)-> Arrow(a,(pop b))
+    match match_with_imp_term (project gl) cciterm with
+	Some (a,b)-> Arrow(a,(pop (EConstr.of_constr b)))
       |_->
-	 match match_with_forall_term cciterm with
+	 match match_with_forall_term (project gl) cciterm with
 	     Some (_,a,b)-> Forall(a,b)
 	   |_->
-	      match match_with_nodep_ind cciterm with
+	      match match_with_nodep_ind (project gl) cciterm with
 		  Some (i,l,n)->
 		    let ind,u=destInd i in
 		    let (mib,mip) = Global.lookup_inductive ind in
@@ -96,7 +96,7 @@ let kind_of_formula gl term =
 			let has_realargs=(n>0) in
 			let is_trivial=
 			  let is_constant c =
-			    Int.equal (nb_prod c) mib.mind_nparams in
+			    Int.equal (nb_prod (project gl) (EConstr.of_constr c)) mib.mind_nparams in
 			    Array.exists is_constant mip.mind_nf_lc in
 			  if Inductiveops.mis_is_recursive (ind,mib,mip) ||
 			    (has_realargs && not is_trivial)
@@ -108,7 +108,7 @@ let kind_of_formula gl term =
 			    else
 			      Or((ind,u),l,is_trivial)
 		| _ ->
-		    match match_with_sigma_type cciterm with
+		    match match_with_sigma_type (project gl) cciterm with
 			Some (i,l)-> Exists((destInd i),l)
 		      |_-> Atom (normalize cciterm)
 
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 7ffc78928d..1d107e9afe 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -38,8 +38,8 @@ let wrap n b continue seq gls=
 	  []->anomaly (Pp.str "Not the expected number of hyps")
 	| nd::q->
             let id = NamedDecl.get_id nd in
-	    if occur_var env id (pf_concl gls) ||
-	      List.exists (occur_var_in_decl env id) ctx then
+	    if occur_var env (project gls) id (EConstr.of_constr (pf_concl gls)) ||
+	      List.exists (occur_var_in_decl env (project gls)  id) ctx then
 		(aux (i-1) q (nd::ctx))
 	    else
 	      add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index d9ab36ad64..01c0197443 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -21,7 +21,10 @@ exception UFAIL of constr*constr
    to the equation set. Raises UFAIL with a pair of  terms
 *)
 
+let strip_outer_cast t = strip_outer_cast Evd.empty (EConstr.of_constr t) (** FIXME *)
+
 let unif t1 t2=
+  let evd = Evd.empty in (** FIXME *)
   let bige=Queue.create ()
   and sigma=ref [] in
   let bind i t=
@@ -47,18 +50,18 @@ let unif t1 t2=
 		else bind i nt2
 	  | Meta i,_ ->
 	      let t=subst_meta !sigma nt2 in
-		if Int.Set.is_empty (free_rels t) &&
-		  not (occur_term (mkMeta i) t) then
+		if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) &&
+		  not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then
 		    bind i t else raise (UFAIL(nt1,nt2))
 	  | _,Meta i ->
 	      let t=subst_meta !sigma nt1 in
-		if Int.Set.is_empty (free_rels t) &&
-		  not (occur_term (mkMeta i) t) then
+		if Int.Set.is_empty (free_rels evd (EConstr.of_constr t)) &&
+		  not (occur_term evd (EConstr.mkMeta i) (EConstr.of_constr t)) then
 		    bind i t else raise (UFAIL(nt1,nt2))
 	  | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
  	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige
 	  | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
-	      Queue.add (a,c) bige;Queue.add (pop b,pop d) bige
+	      Queue.add (a,c) bige;Queue.add (pop (EConstr.of_constr b),pop (EConstr.of_constr d)) bige
 	  | Case (_,pa,ca,va),Case (_,pb,cb,vb)->
 	      Queue.add (pa,pb) bige;
 	      Queue.add (ca,cb) bige;
-- 
cgit v1.2.3


From 8f6aab1f4d6d60842422abc5217daac806eb0897 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 1 Nov 2016 20:53:32 +0100
Subject: Reductionops API using EConstr.

---
 plugins/firstorder/instances.ml | 2 +-
 plugins/firstorder/unify.ml     | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index eebd974ea8..a3513692c5 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -107,7 +107,7 @@ let mk_open_instance id idc gl m t=
       let typ=pf_unsafe_type_of gl idc in
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
-      let (nam,_,_)=destProd (whd_all env evmap typ) in
+      let (nam,_,_)=destProd (whd_all env evmap (EConstr.of_constr typ)) in
 	match nam with
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 01c0197443..fb237f29bf 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -41,8 +41,8 @@ let unif t1 t2=
     Queue.add (t1,t2) bige;
     try while true do
       let t1,t2=Queue.take bige in
-      let nt1=head_reduce (whd_betaiotazeta Evd.empty t1)
-      and nt2=head_reduce (whd_betaiotazeta Evd.empty t2) in
+      let nt1=head_reduce (whd_betaiotazeta Evd.empty (EConstr.of_constr t1))
+      and nt2=head_reduce (whd_betaiotazeta Evd.empty (EConstr.of_constr t2)) in
 	match (kind_of_term nt1),(kind_of_term nt2) with
 	    Meta i,Meta j->
 	      if not (Int.equal i j) then
-- 
cgit v1.2.3


From e27949240f5b1ee212e7d0fe3326a21a13c4abb0 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 6 Nov 2016 17:21:44 +0100
Subject: Typing API using EConstr.

---
 plugins/firstorder/instances.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a3513692c5..44bdb585a1 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -155,7 +155,7 @@ let left_instance_tac (inst,id) continue seq=
 		    it_mkLambda_or_LetIn
 		      (mkApp(idc,[|ot|])) rc in
 		  let evmap, _ =
-		    try Typing.type_of (pf_env gl) evmap gt
+		    try Typing.type_of (pf_env gl) evmap (EConstr.of_constr gt)
 		    with e when CErrors.noncritical e ->
 		      error "Untypable instance, maybe higher-order non-prenex quantification" in
 		    tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
-- 
cgit v1.2.3


From 67dc22d8389234d0c9b329944ff579e7056b7250 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Tue, 8 Nov 2016 10:57:05 +0100
Subject: Cases API using EConstr.

---
 plugins/firstorder/formula.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 79f185d187..60e9196afa 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -54,7 +54,7 @@ let construct_nhyps ind gls =
 let ind_hyps nevar ind largs gls=
   let types= Inductiveops.arities_of_constructors (pf_env gls) ind in
   let myhyps t =
-    let t1=prod_applist t largs in
+    let t1=Term.prod_applist t largs in
     let t2=snd (decompose_prod_n_assum nevar t1) in
       fst (decompose_prod_assum t2) in
     Array.map myhyps types
-- 
cgit v1.2.3


From cbea91d815f134d63d02d8fb1bd78ed97db28cd1 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 11 Nov 2016 19:52:48 +0100
Subject: Tacmach API using EConstr.

---
 plugins/firstorder/instances.ml | 2 +-
 plugins/firstorder/sequent.ml   | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 44bdb585a1..6c245063c8 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -104,7 +104,7 @@ let mk_open_instance id idc gl m t=
   let evmap=Refiner.project gl in
   let var_id=
     if id==dummy_id then dummy_bvid else
-      let typ=pf_unsafe_type_of gl idc in
+      let typ=pf_unsafe_type_of gl (EConstr.of_constr idc) in
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
       let (nam,_,_)=destProd (whd_all env evmap (EConstr.of_constr typ)) in
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 1248b60a76..87e7192d78 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -200,7 +200,7 @@ let extend_with_ref_list l seq gl =
   let l = expand_constructor_hints l in
   let f gr (seq,gl) =
     let gl, c = pf_eapply Evd.fresh_global gl gr in
-    let typ=(pf_unsafe_type_of gl c) in
+    let typ=(pf_unsafe_type_of gl (EConstr.of_constr c)) in
       (add_formula Hyp gr typ seq gl,gl) in
     List.fold_right f l (seq,gl)
 
@@ -215,7 +215,7 @@ let extend_with_auto_hints l seq gl=
           let (c, _, _) = c in
 	  (try
 	     let gr = global_of_constr c in
-	     let typ=(pf_unsafe_type_of gl c) in
+	     let typ=(pf_unsafe_type_of gl (EConstr.of_constr c)) in
 	       seqref:=add_formula Hint gr typ !seqref gl
 	   with Not_found->())
       | _-> () in
-- 
cgit v1.2.3


From 771be16883c8c47828f278ce49545716918764c4 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 12 Nov 2016 01:52:15 +0100
Subject: Hipattern API using EConstr.

---
 plugins/firstorder/formula.ml | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 60e9196afa..96b991e1fd 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -79,15 +79,16 @@ type kind_of_formula=
 let kind_of_formula gl term =
   let normalize=special_nf gl in
   let cciterm=special_whd gl term in
-    match match_with_imp_term (project gl) cciterm with
-	Some (a,b)-> Arrow(a,(pop (EConstr.of_constr b)))
+    match match_with_imp_term (project gl) (EConstr.of_constr cciterm) with
+	Some (a,b)-> Arrow(EConstr.Unsafe.to_constr a,(pop b))
       |_->
-	 match match_with_forall_term (project gl) cciterm with
-	     Some (_,a,b)-> Forall(a,b)
+	 match match_with_forall_term (project gl) (EConstr.of_constr cciterm) with
+	     Some (_,a,b)-> Forall(EConstr.Unsafe.to_constr a,EConstr.Unsafe.to_constr b)
 	   |_->
-	      match match_with_nodep_ind (project gl) cciterm with
+	      match match_with_nodep_ind (project gl) (EConstr.of_constr cciterm) with
 		  Some (i,l,n)->
-		    let ind,u=destInd i in
+                    let l = List.map EConstr.Unsafe.to_constr l in
+		    let ind,u=EConstr.destInd (project gl) i in
 		    let (mib,mip) = Global.lookup_inductive ind in
 		    let nconstr=Array.length mip.mind_consnames in
 		      if Int.equal nconstr 0 then
@@ -108,8 +109,8 @@ let kind_of_formula gl term =
 			    else
 			      Or((ind,u),l,is_trivial)
 		| _ ->
-		    match match_with_sigma_type (project gl) cciterm with
-			Some (i,l)-> Exists((destInd i),l)
+		    match match_with_sigma_type (project gl) (EConstr.of_constr cciterm) with
+			Some (i,l)-> Exists((EConstr.destInd (project gl) i),List.map EConstr.Unsafe.to_constr l)
 		      |_-> Atom (normalize cciterm)
 
 type atoms = {positive:constr list;negative:constr list}
-- 
cgit v1.2.3


From 485bbfbed4ae4a28119c4e42c5e40fd77abf4f8a Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 13 Nov 2016 20:38:41 +0100
Subject: Tactics API using EConstr.

---
 plugins/firstorder/instances.ml | 18 ++++++++++--------
 plugins/firstorder/rules.ml     | 27 ++++++++++++++-------------
 2 files changed, 24 insertions(+), 21 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 6c245063c8..a320b47aa3 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -117,6 +117,7 @@ let mk_open_instance id idc gl m t=
       let nid=(fresh_id avoid var_id gl) in
       let evmap = Sigma.Unsafe.of_evar_map evmap in
       let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
+      let c = EConstr.Unsafe.to_constr c in
       let evmap = Sigma.to_evar_map evmap in
       let decl = LocalAssum (Name nid, c) in
 	aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in
@@ -131,13 +132,13 @@ let left_instance_tac (inst,id) continue seq=
 	if lookup (id,None) seq then
 	  tclFAIL 0 (Pp.str "already done")
 	else
-	  tclTHENS (Proofview.V82.of_tactic (cut dom))
+	  tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr dom)))
 	    [tclTHENLIST
 	       [Proofview.V82.of_tactic introf;
                 pf_constr_of_global id (fun idc ->
 		(fun gls-> Proofview.V82.of_tactic (generalize
-		   [mkApp(idc,
-			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])]) gls));
+		   [EConstr.of_constr (mkApp(idc,
+			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|]))]) gls));
 		Proofview.V82.of_tactic introf;
 		tclSOLVE [wrap 1 false continue
 			    (deepen (record (id,None) seq))]];
@@ -154,14 +155,15 @@ let left_instance_tac (inst,id) continue seq=
 		  let gt=
 		    it_mkLambda_or_LetIn
 		      (mkApp(idc,[|ot|])) rc in
+                  let gt = EConstr.of_constr gt in
 		  let evmap, _ =
-		    try Typing.type_of (pf_env gl) evmap (EConstr.of_constr gt)
+		    try Typing.type_of (pf_env gl) evmap gt
 		    with e when CErrors.noncritical e ->
 		      error "Untypable instance, maybe higher-order non-prenex quantification" in
 		    tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
 	    else
 	      pf_constr_of_global id (fun idc ->
-		Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])]))
+		Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(idc,[|t|]))]))
 	  in
 	    tclTHENLIST
 	      [special_generalize;
@@ -172,16 +174,16 @@ let left_instance_tac (inst,id) continue seq=
 let right_instance_tac inst continue seq=
   match inst with
       Phantom dom ->
-	tclTHENS (Proofview.V82.of_tactic (cut dom))
+	tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr dom)))
 	[tclTHENLIST
 	   [Proofview.V82.of_tactic introf;
 	    (fun gls->
 	       Proofview.V82.of_tactic (split (ImplicitBindings
-			[mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls);
+			[EConstr.mkVar (Tacmach.pf_nth_hyp_id gls 1)])) gls);
 	    tclSOLVE [wrap 0 true continue (deepen seq)]];
 	 tclTRY (Proofview.V82.of_tactic assumption)]
     | Real ((0,t),_) ->
-	(tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [t])))
+	(tclTHEN (Proofview.V82.of_tactic (split (ImplicitBindings [EConstr.of_constr t])))
 	   (tclSOLVE [wrap 0 true continue (deepen seq)]))
     | Real ((m,t),_) ->
 	tclFAIL 0 (Pp.str "not implemented ... yet")
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 1d107e9afe..bed7a727f7 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -59,7 +59,7 @@ let clear_global=function
 (* connection rules *)
 
 let axiom_tac t seq=
-  try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check c))
+  try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check (EConstr.of_constr c)))
   with Not_found->tclFAIL 0 (Pp.str "No axiom link")
 
 let ll_atom_tac a backtrack id continue seq=
@@ -68,7 +68,7 @@ let ll_atom_tac a backtrack id continue seq=
       tclTHENLIST
 	[pf_constr_of_global (find_left a seq) (fun left ->
 	  pf_constr_of_global id (fun id -> 
-	    Proofview.V82.of_tactic (generalize [mkApp(id, [|left|])])));
+	    Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(id, [|left|]))])));
 	 clear_global id;
 	 Proofview.V82.of_tactic intro]
     with Not_found->tclFAIL 0 (Pp.str "No link"))
@@ -95,7 +95,7 @@ let left_and_tac ind backtrack id continue seq gls=
  let n=(construct_nhyps ind gls).(0) in
    tclIFTHENELSE
      (tclTHENLIST
-      [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim);
+      [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim));
        clear_global id;
        tclDO n (Proofview.V82.of_tactic intro)])
      (wrap n false continue seq)
@@ -109,12 +109,12 @@ let left_or_tac ind backtrack id continue seq gls=
        tclDO n (Proofview.V82.of_tactic intro);
        wrap n false continue seq] in
     tclIFTHENSVELSE
-      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
+      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim)))
       (Array.map f v)
       backtrack gls
 
 let left_false_tac id=
-  Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)
+  Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim))
 
 (* left arrow connective rules *)
 
@@ -131,7 +131,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
        let vars=Array.init p (fun j->mkRel (p-j)) in
        let capply=mkApp ((lift p cstr),vars) in
        let head=mkApp ((lift p idc),[|capply|]) in
-         it_mkLambda_or_LetIn head rc in
+         EConstr.of_constr (it_mkLambda_or_LetIn head rc) in
        let lp=Array.length rcs in
        let newhyps idc =List.init lp (myterm idc) in
 	 tclIFTHENELSE
@@ -143,16 +143,16 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
 
 let ll_arrow_tac a b c backtrack id continue seq=
   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 d idc =EConstr.of_constr (mkLambda (Anonymous,b,
+		  mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|]))) in
     tclORELSE
-      (tclTHENS (Proofview.V82.of_tactic (cut c))
+      (tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr c)))
 	 [tclTHENLIST
 	    [Proofview.V82.of_tactic introf;
 	     clear_global id;
 	     wrap 1 false continue seq];
-	  tclTHENS (Proofview.V82.of_tactic (cut cc))
-            [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c));
+	  tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr cc)))
+            [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check (EConstr.of_constr c)));
 	     tclTHENLIST
 	       [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc]));
 		clear_global id;
@@ -177,7 +177,7 @@ let forall_tac backtrack continue seq=
 let left_exists_tac ind backtrack id continue seq gls=
   let n=(construct_nhyps ind gls).(0) in
     tclIFTHENELSE
-      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
+      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim)))
       (tclTHENLIST [clear_global id;
                     tclDO n (Proofview.V82.of_tactic intro);
                     (wrap (n-1) false continue seq)])
@@ -186,13 +186,14 @@ let left_exists_tac ind backtrack id continue seq gls=
 
 let ll_forall_tac prod backtrack id continue seq=
   tclORELSE
-    (tclTHENS (Proofview.V82.of_tactic (cut prod))
+    (tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr prod)))
        [tclTHENLIST
 	  [Proofview.V82.of_tactic intro;
            pf_constr_of_global id (fun idc ->
 	   (fun gls->
 	      let id0=pf_nth_hyp_id gls 1 in
               let term=mkApp(idc,[|mkVar(id0)|]) in
+              let term = EConstr.of_constr term in
 		tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls));
 	   clear_global id;
 	   Proofview.V82.of_tactic intro;
-- 
cgit v1.2.3


From 34e86e839be251717db96f1f5969d7724ab43097 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 19 Nov 2016 02:45:54 +0100
Subject: Hints API using EConstr.

---
 plugins/firstorder/sequent.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 87e7192d78..91cd102a23 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -214,8 +214,8 @@ let extend_with_auto_hints l seq gl=
       | Res_pf_THEN_trivial_fail (c,_) ->
           let (c, _, _) = c in
 	  (try
-	     let gr = global_of_constr c in
-	     let typ=(pf_unsafe_type_of gl (EConstr.of_constr c)) in
+	     let (gr, _) = Termops.global_of_constr (project gl) c in
+	     let typ=(pf_unsafe_type_of gl c) in
 	       seqref:=add_formula Hint gr typ !seqref gl
 	   with Not_found->())
       | _-> () in
-- 
cgit v1.2.3


From d4b344acb23f19b089098b7788f37ea22bc07b81 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sun, 20 Nov 2016 20:09:26 +0100
Subject: Eliminating parts of the right-hand side compatibility layer

---
 plugins/firstorder/unify.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index fb237f29bf..205cb282d1 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -21,7 +21,8 @@ exception UFAIL of constr*constr
    to the equation set. Raises UFAIL with a pair of  terms
 *)
 
-let strip_outer_cast t = strip_outer_cast Evd.empty (EConstr.of_constr t) (** FIXME *)
+let strip_outer_cast t =
+  EConstr.Unsafe.to_constr (strip_outer_cast Evd.empty (EConstr.of_constr t)) (** FIXME *)
 
 let unif t1 t2=
   let evd = Evd.empty in (** FIXME *)
-- 
cgit v1.2.3


From 0cdb7e42f64674e246d4e24e3c725e23ceeec6bd Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Mon, 21 Nov 2016 12:13:05 +0100
Subject: Reductionops now return EConstrs.

---
 plugins/firstorder/instances.ml | 2 +-
 plugins/firstorder/unify.ml     | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index a320b47aa3..24d4346d9a 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -107,7 +107,7 @@ let mk_open_instance id idc gl m t=
       let typ=pf_unsafe_type_of gl (EConstr.of_constr idc) in
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
-      let (nam,_,_)=destProd (whd_all env evmap (EConstr.of_constr typ)) in
+      let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap (EConstr.of_constr typ))) in
 	match nam with
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 205cb282d1..5520c7e35d 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -42,8 +42,8 @@ let unif t1 t2=
     Queue.add (t1,t2) bige;
     try while true do
       let t1,t2=Queue.take bige in
-      let nt1=head_reduce (whd_betaiotazeta Evd.empty (EConstr.of_constr t1))
-      and nt2=head_reduce (whd_betaiotazeta Evd.empty (EConstr.of_constr t2)) in
+      let nt1=head_reduce (EConstr.Unsafe.to_constr (whd_betaiotazeta evd (EConstr.of_constr t1)))
+      and nt2=head_reduce (EConstr.Unsafe.to_constr (whd_betaiotazeta evd (EConstr.of_constr t2))) in
 	match (kind_of_term nt1),(kind_of_term nt2) with
 	    Meta i,Meta j->
 	      if not (Int.equal i j) then
-- 
cgit v1.2.3


From b36adb2124d3ba8a5547605e7f89bb0835d0ab10 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Nov 2016 15:50:17 +0100
Subject: Removing some return type compatibility layers in Termops.

---
 plugins/firstorder/formula.ml | 4 +++-
 plugins/firstorder/unify.ml   | 4 +++-
 2 files changed, 6 insertions(+), 2 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 96b991e1fd..87bac2fe39 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -76,11 +76,13 @@ type kind_of_formula=
   | Forall of constr*constr
   | Atom of constr
 
+let pop t = Vars.lift (-1) t
+
 let kind_of_formula gl term =
   let normalize=special_nf gl in
   let cciterm=special_whd gl term in
     match match_with_imp_term (project gl) (EConstr.of_constr cciterm) with
-	Some (a,b)-> Arrow(EConstr.Unsafe.to_constr a,(pop b))
+	Some (a,b)-> Arrow(EConstr.Unsafe.to_constr a,(pop (EConstr.Unsafe.to_constr b)))
       |_->
 	 match match_with_forall_term (project gl) (EConstr.of_constr cciterm) with
 	     Some (_,a,b)-> Forall(EConstr.Unsafe.to_constr a,EConstr.Unsafe.to_constr b)
diff --git a/plugins/firstorder/unify.ml b/plugins/firstorder/unify.ml
index 5520c7e35d..7cbfb8e7de 100644
--- a/plugins/firstorder/unify.ml
+++ b/plugins/firstorder/unify.ml
@@ -24,6 +24,8 @@ exception UFAIL of constr*constr
 let strip_outer_cast t =
   EConstr.Unsafe.to_constr (strip_outer_cast Evd.empty (EConstr.of_constr t)) (** FIXME *)
 
+let pop t = Vars.lift (-1) t
+
 let unif t1 t2=
   let evd = Evd.empty in (** FIXME *)
   let bige=Queue.create ()
@@ -62,7 +64,7 @@ let unif t1 t2=
 	  | Cast(_,_,_),_->Queue.add (strip_outer_cast nt1,nt2) bige
  	  | _,Cast(_,_,_)->Queue.add (nt1,strip_outer_cast nt2) bige
 	  | (Prod(_,a,b),Prod(_,c,d))|(Lambda(_,a,b),Lambda(_,c,d))->
-	      Queue.add (a,c) bige;Queue.add (pop (EConstr.of_constr b),pop (EConstr.of_constr d)) bige
+	      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;
-- 
cgit v1.2.3


From 02dd160233adc784eac732d97a88356d1f0eaf9b Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Nov 2016 18:34:53 +0100
Subject: Removing various compatibility layers of tactics.

---
 plugins/firstorder/instances.ml | 2 +-
 plugins/firstorder/rules.ml     | 4 ++--
 plugins/firstorder/sequent.ml   | 2 ++
 3 files changed, 5 insertions(+), 3 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 24d4346d9a..2881b53339 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -107,7 +107,7 @@ let mk_open_instance id idc gl m t=
       let typ=pf_unsafe_type_of gl (EConstr.of_constr idc) in
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
-      let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap (EConstr.of_constr typ))) in
+      let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap typ)) in
 	match nam with
 	    Name id -> id
 	  | Anonymous ->  dummy_bvid in
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index bed7a727f7..38dae0b204 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -38,14 +38,14 @@ let wrap n b continue seq gls=
 	  []->anomaly (Pp.str "Not the expected number of hyps")
 	| nd::q->
             let id = NamedDecl.get_id nd in
-	    if occur_var env (project gls) id (EConstr.of_constr (pf_concl gls)) ||
+	    if occur_var env (project gls) id (pf_concl gls) ||
 	      List.exists (occur_var_in_decl env (project gls)  id) ctx then
 		(aux (i-1) q (nd::ctx))
 	    else
 	      add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in
   let seq1=aux n nc [] in
   let seq2=if b then
-    add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in
+    add_formula Concl dummy_id (EConstr.Unsafe.to_constr (pf_concl gls)) seq1 gls else seq1 in
     continue seq2 gls
 
 let basename_of_global=function
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 91cd102a23..fb0c22c2b7 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -201,6 +201,7 @@ let extend_with_ref_list l seq gl =
   let f gr (seq,gl) =
     let gl, c = pf_eapply Evd.fresh_global gl gr in
     let typ=(pf_unsafe_type_of gl (EConstr.of_constr c)) in
+    let typ = EConstr.Unsafe.to_constr typ in
       (add_formula Hyp gr typ seq gl,gl) in
     List.fold_right f l (seq,gl)
 
@@ -216,6 +217,7 @@ let extend_with_auto_hints l seq gl=
 	  (try
 	     let (gr, _) = Termops.global_of_constr (project gl) c in
 	     let typ=(pf_unsafe_type_of gl c) in
+	     let typ = EConstr.Unsafe.to_constr typ in
 	       seqref:=add_formula Hint gr typ !seqref gl
 	   with Not_found->())
       | _-> () in
-- 
cgit v1.2.3


From 01849481fbabc3a3fa6c483e703996b01e37fca5 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 01:25:11 +0100
Subject: Removing compatibility layers from Tacticals

---
 plugins/firstorder/instances.ml | 12 +++++++-----
 plugins/firstorder/rules.ml     | 32 +++++++++++++++++++-------------
 2 files changed, 26 insertions(+), 18 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 2881b53339..ef8172de41 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -104,7 +104,7 @@ let mk_open_instance id idc gl m t=
   let evmap=Refiner.project gl in
   let var_id=
     if id==dummy_id then dummy_bvid else
-      let typ=pf_unsafe_type_of gl (EConstr.of_constr idc) in
+      let typ=pf_unsafe_type_of gl idc in
 	(* since we know we will get a product,
 	   reduction is not too expensive *)
       let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap typ)) in
@@ -127,6 +127,7 @@ let mk_open_instance id idc gl m t=
 (* tactics   *)
 
 let left_instance_tac (inst,id) continue seq=
+  let open EConstr in
   match inst with
       Phantom dom->
 	if lookup (id,None) seq then
@@ -137,8 +138,8 @@ let left_instance_tac (inst,id) continue seq=
 	       [Proofview.V82.of_tactic introf;
                 pf_constr_of_global id (fun idc ->
 		(fun gls-> Proofview.V82.of_tactic (generalize
-		   [EConstr.of_constr (mkApp(idc,
-			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|]))]) gls));
+		   [mkApp(idc,
+			  [|mkVar (Tacmach.pf_nth_hyp_id gls 1)|])]) gls));
 		Proofview.V82.of_tactic introf;
 		tclSOLVE [wrap 1 false continue
 			    (deepen (record (id,None) seq))]];
@@ -152,18 +153,19 @@ let left_instance_tac (inst,id) continue seq=
 	      pf_constr_of_global id (fun idc ->
 		fun gl->
 		  let evmap,rc,ot = mk_open_instance id idc gl m t in
+		  let ot = EConstr.of_constr ot in
 		  let gt=
 		    it_mkLambda_or_LetIn
 		      (mkApp(idc,[|ot|])) rc in
-                  let gt = EConstr.of_constr gt in
 		  let evmap, _ =
 		    try Typing.type_of (pf_env gl) evmap gt
 		    with e when CErrors.noncritical e ->
 		      error "Untypable instance, maybe higher-order non-prenex quantification" in
 		    tclTHEN (Refiner.tclEVARS evmap) (Proofview.V82.of_tactic (generalize [gt])) gl)
 	    else
+              let t = EConstr.of_constr t in
 	      pf_constr_of_global id (fun idc ->
-		Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(idc,[|t|]))]))
+		Proofview.V82.of_tactic (generalize [mkApp(idc,[|t|])]))
 	  in
 	    tclTHENLIST
 	      [special_generalize;
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 38dae0b204..36bd91ab6a 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -59,16 +59,17 @@ let clear_global=function
 (* connection rules *)
 
 let axiom_tac t seq=
-  try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check (EConstr.of_constr c)))
+  try pf_constr_of_global (find_left t seq) (fun c -> Proofview.V82.of_tactic (exact_no_check c))
   with Not_found->tclFAIL 0 (Pp.str "No axiom link")
 
 let ll_atom_tac a backtrack id continue seq=
+  let open EConstr in
   tclIFTHENELSE
     (try
       tclTHENLIST
 	[pf_constr_of_global (find_left a seq) (fun left ->
 	  pf_constr_of_global id (fun id -> 
-	    Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(id, [|left|]))])));
+	    Proofview.V82.of_tactic (generalize [(mkApp(id, [|left|]))])));
 	 clear_global id;
 	 Proofview.V82.of_tactic intro]
     with Not_found->tclFAIL 0 (Pp.str "No link"))
@@ -95,7 +96,7 @@ let left_and_tac ind backtrack id continue seq gls=
  let n=(construct_nhyps ind gls).(0) in
    tclIFTHENELSE
      (tclTHENLIST
-      [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim));
+      [Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim);
        clear_global id;
        tclDO n (Proofview.V82.of_tactic intro)])
      (wrap n false continue seq)
@@ -109,12 +110,12 @@ let left_or_tac ind backtrack id continue seq gls=
        tclDO n (Proofview.V82.of_tactic intro);
        wrap n false continue seq] in
     tclIFTHENSVELSE
-      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim)))
+      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
       (Array.map f v)
       backtrack gls
 
 let left_false_tac id=
-  Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim))
+  Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim)
 
 (* left arrow connective rules *)
 
@@ -133,7 +134,7 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
        let head=mkApp ((lift p idc),[|capply|]) in
          EConstr.of_constr (it_mkLambda_or_LetIn head rc) in
        let lp=Array.length rcs in
-       let newhyps idc =List.init lp (myterm idc) in
+       let newhyps idc =List.init lp (myterm (EConstr.Unsafe.to_constr idc)) in
 	 tclIFTHENELSE
 	   (tclTHENLIST
 	      [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize (newhyps idc)));
@@ -142,17 +143,22 @@ let ll_ind_tac (ind,u as indu) largs backtrack id continue seq gl=
 	   (wrap lp false continue seq) backtrack gl
 
 let ll_arrow_tac a b c backtrack id continue seq=
+  let open EConstr in
+  let open Vars in
+  let a = EConstr.of_constr a in
+  let b = EConstr.of_constr b in
+  let c = EConstr.of_constr c in
   let cc=mkProd(Anonymous,a,(lift 1 b)) in
-  let d idc =EConstr.of_constr (mkLambda (Anonymous,b,
-		  mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|]))) in
+  let d idc = mkLambda (Anonymous,b,
+		  mkApp (idc, [|mkLambda (Anonymous,(lift 1 a),(mkRel 2))|])) in
     tclORELSE
-      (tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr c)))
+      (tclTHENS (Proofview.V82.of_tactic (cut c))
 	 [tclTHENLIST
 	    [Proofview.V82.of_tactic introf;
 	     clear_global id;
 	     wrap 1 false continue seq];
-	  tclTHENS (Proofview.V82.of_tactic (cut (EConstr.of_constr cc)))
-            [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check (EConstr.of_constr c)));
+	  tclTHENS (Proofview.V82.of_tactic (cut cc))
+            [pf_constr_of_global id (fun c -> Proofview.V82.of_tactic (exact_no_check c));
 	     tclTHENLIST
 	       [pf_constr_of_global id (fun idc -> Proofview.V82.of_tactic (generalize [d idc]));
 		clear_global id;
@@ -177,7 +183,7 @@ let forall_tac backtrack continue seq=
 let left_exists_tac ind backtrack id continue seq gls=
   let n=(construct_nhyps ind gls).(0) in
     tclIFTHENELSE
-      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id (EConstr.of_constr %> simplest_elim)))
+      (Proofview.V82.of_tactic (Tacticals.New.pf_constr_of_global id simplest_elim))
       (tclTHENLIST [clear_global id;
                     tclDO n (Proofview.V82.of_tactic intro);
                     (wrap (n-1) false continue seq)])
@@ -191,9 +197,9 @@ let ll_forall_tac prod backtrack id continue seq=
 	  [Proofview.V82.of_tactic intro;
            pf_constr_of_global id (fun idc ->
 	   (fun gls->
+              let open EConstr in
 	      let id0=pf_nth_hyp_id gls 1 in
               let term=mkApp(idc,[|mkVar(id0)|]) in
-              let term = EConstr.of_constr term in
 		tclTHEN (Proofview.V82.of_tactic (generalize [term])) (Proofview.V82.of_tactic (clear [id0])) gls));
 	   clear_global id;
 	   Proofview.V82.of_tactic intro;
-- 
cgit v1.2.3


From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 16:18:47 +0100
Subject: Definining EConstr-based contexts.

This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.
---
 plugins/firstorder/instances.ml | 3 +--
 plugins/firstorder/rules.ml     | 2 +-
 2 files changed, 2 insertions(+), 3 deletions(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index ef8172de41..9dc2a51a61 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -117,10 +117,9 @@ let mk_open_instance id idc gl m t=
       let nid=(fresh_id avoid var_id gl) in
       let evmap = Sigma.Unsafe.of_evar_map evmap in
       let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
-      let c = EConstr.Unsafe.to_constr c in
       let evmap = Sigma.to_evar_map evmap in
       let decl = LocalAssum (Name nid, c) in
-	aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in
+	aux (n-1) (nid::avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
   let evmap, decls = aux m [] env evmap [] in
     evmap, decls, revt
 
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 36bd91ab6a..a60fd4d8f1 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -42,7 +42,7 @@ let wrap n b continue seq gls=
 	      List.exists (occur_var_in_decl env (project gls)  id) ctx then
 		(aux (i-1) q (nd::ctx))
 	    else
-	      add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in
+	      add_formula Hyp (VarRef id) (EConstr.Unsafe.to_constr (NamedDecl.get_type nd)) (aux (i-1) q (nd::ctx)) gls in
   let seq1=aux n nc [] in
   let seq2=if b then
     add_formula Concl dummy_id (EConstr.Unsafe.to_constr (pf_concl gls)) seq1 gls else seq1 in
-- 
cgit v1.2.3


From 7babf0d42af11f5830bc157a671bd81b478a4f02 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 1 Apr 2017 02:36:16 +0200
Subject: Using delayed universe instances in EConstr.

The transition has been done a bit brutally. I think we can still save a
lot of useless normalizations here and there by providing the right API
in EConstr. Nonetheless, this is a first step.
---
 plugins/firstorder/formula.ml | 6 +++++-
 1 file changed, 5 insertions(+), 1 deletion(-)

(limited to 'plugins/firstorder')

diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 87bac2fe39..7773f6a2fd 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -91,6 +91,7 @@ let kind_of_formula gl term =
 		  Some (i,l,n)->
                     let l = List.map EConstr.Unsafe.to_constr l in
 		    let ind,u=EConstr.destInd (project gl) i in
+		    let u = EConstr.EInstance.kind (project gl) u in
 		    let (mib,mip) = Global.lookup_inductive ind in
 		    let nconstr=Array.length mip.mind_consnames in
 		      if Int.equal nconstr 0 then
@@ -112,7 +113,10 @@ let kind_of_formula gl term =
 			      Or((ind,u),l,is_trivial)
 		| _ ->
 		    match match_with_sigma_type (project gl) (EConstr.of_constr cciterm) with
-			Some (i,l)-> Exists((EConstr.destInd (project gl) i),List.map EConstr.Unsafe.to_constr l)
+			Some (i,l)->
+                          let (ind, u) = EConstr.destInd (project gl) i in
+                          let u = EConstr.EInstance.kind (project gl) u in
+                          Exists((ind, u), List.map EConstr.Unsafe.to_constr l)
 		      |_-> Atom (normalize cciterm)
 
 type atoms = {positive:constr list;negative:constr list}
-- 
cgit v1.2.3