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/funind/invfun.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index c8b4e48337..cf42a809db 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -254,7 +254,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
     let princ_type =  nf_zeta princ_type in
     let princ_infos = Tactics.compute_elim_sig princ_type in
     (* The number of args of the function is then easily computable *)
-    let nb_fun_args = nb_prod (pf_concl g)  - 2  in
+    let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in
     let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
     let ids = args_names@(pf_ids_of_hyps g) in
     (* Since we cannot ensure that the functional principle is defined in the
@@ -467,7 +467,7 @@ let generalize_dependent_of x hyp g =
   tclMAP
     (function
        | LocalAssum (id,t) when not (Id.equal id hyp) &&
-	   (Termops.occur_var (pf_env g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
+	   (Termops.occur_var (pf_env g) (project g) x (EConstr.of_constr t)) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
        | _ -> tclIDTAC
     )
     (pf_hyps g)
@@ -666,7 +666,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     (* Then we get the number of argument of the function
        and compute a fresh name for each of them
     *)
-    let nb_fun_args = nb_prod (pf_concl g)  - 2  in
+    let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in
     let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
     let ids = args_names@(pf_ids_of_hyps g) in
     (* and fresh names for res H and the principle (cf bug bug #1174) *)
@@ -684,7 +684,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	(fun decl ->
 	   List.map
 	     (fun id -> id)
-	     (generate_fresh_id (Id.of_string "y") ids (nb_prod (RelDecl.get_type decl)))
+	     (generate_fresh_id (Id.of_string "y") ids (nb_prod (project g) (EConstr.of_constr (RelDecl.get_type decl))))
 	)
 	branches
     in
-- 
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/funind/invfun.ml | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index cf42a809db..9abe604025 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -251,7 +251,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
     let mib,_ = Global.lookup_inductive graph_ind in
     (* and the principle to use in this lemma in $\zeta$ normal form *)
     let f_principle,princ_type = schemes.(i) in
-    let princ_type =  nf_zeta princ_type in
+    let princ_type =  nf_zeta (EConstr.of_constr princ_type) in
     let princ_infos = Tactics.compute_elim_sig princ_type in
     (* The number of args of the function is then easily computable *)
     let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in
@@ -428,7 +428,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) decl p ->
 	     let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in
-	     (nf_zeta p)::bindings,id::avoid)
+	     (nf_zeta (EConstr.of_constr p))::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
 	  (lemmas)))
@@ -496,7 +496,7 @@ and intros_with_rewrite_aux : tactic =
 	      begin
 		match kind_of_term t with
 		  | App(eq,args) when (eq_constr eq eq_ind)  ->
- 		      if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2)
+ 		      if Reductionops.is_conv (pf_env g) (project g) (EConstr.of_constr args.(1)) (EConstr.of_constr args.(2))
 		      then
 			let id = pf_get_new_id (Id.of_string "y") g  in
 			tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g
@@ -655,12 +655,12 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     *)
     let lemmas =
       Array.map
-	(fun (_,(ctxt,concl)) -> nf_zeta (Termops.it_mkLambda_or_LetIn concl ctxt))
+	(fun (_,(ctxt,concl)) -> nf_zeta (EConstr.of_constr (Termops.it_mkLambda_or_LetIn concl ctxt)))
 	lemmas_types_infos
     in
     (* We get the constant and the principle corresponding to this lemma *)
     let f = funcs.(i) in
-    let graph_principle = nf_zeta schemes.(i)  in
+    let graph_principle = nf_zeta (EConstr.of_constr schemes.(i))  in
     let princ_type = pf_unsafe_type_of g graph_principle in
     let princ_infos = Tactics.compute_elim_sig princ_type in
     (* Then we get the number of argument of the function
@@ -793,7 +793,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 graphs_constr.(i) <- graph;
 	 let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
 	 let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in 
-	   let type_of_lemma = nf_zeta type_of_lemma in
+	   let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
 	   observe (str "type_of_lemma := " ++ Printer.pr_lconstr_env (Global.env ()) !evd type_of_lemma);
 	   type_of_lemma,type_info
 	)
@@ -860,7 +860,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let type_of_lemma =
 	   Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
 	 in
-	 let type_of_lemma = nf_zeta type_of_lemma in
+	 let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
 	 observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma);
 	 type_of_lemma,type_info
 	)
-- 
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/funind/invfun.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 9abe604025..e5286fb1fd 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -134,7 +134,7 @@ let generate_type evd g_to_f f graph i =
     Evd.fresh_global  (Global.env ()) !evd  (Globnames.IndRef (fst (destInd graph)))
   in
   evd:=evd';
-  let graph_arity = Typing.e_type_of (Global.env ()) evd graph in
+  let graph_arity = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr graph) in
   let ctxt,_ = decompose_prod_assum graph_arity in
   let fun_ctxt,res_type =
     match ctxt with
@@ -202,7 +202,7 @@ let find_induction_principle evd f =
     | None -> raise Not_found
     | Some rect_lemma ->
        let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (Globnames.ConstRef rect_lemma) in
-       let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
+       let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr rect_lemma) in
        evd:=evd';
        rect_lemma,typ
 
@@ -449,7 +449,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	     "functional_induction" (
 	       (fun gl ->
 		let term = mkApp (mkVar principle_id,Array.of_list bindings) in
-		let gl', _ty = pf_eapply (Typing.type_of ~refresh:true)  gl term in
+		let gl', _ty = pf_eapply (Typing.type_of ~refresh:true)  gl (EConstr.of_constr term) in
 		Proofview.V82.of_tactic (apply term) gl')
 	   ))
 	  (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
@@ -792,7 +792,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
 	 graphs_constr.(i) <- graph;
 	 let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
-	 let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in 
+	 let _ = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr type_of_lemma) in 
 	   let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
 	   observe (str "type_of_lemma := " ++ Printer.pr_lconstr_env (Global.env ()) !evd type_of_lemma);
 	   type_of_lemma,type_info
-- 
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/funind/invfun.ml | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index e5286fb1fd..6359255626 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -305,7 +305,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       let constructor_args g =
 	List.fold_right 
 	  (fun hid acc ->
-	     let type_of_hid = pf_unsafe_type_of g (mkVar hid) in
+	     let type_of_hid = pf_unsafe_type_of g (EConstr.mkVar hid) in
 	     match kind_of_term type_of_hid with
 	       | Prod(_,_,t') ->
 		   begin
@@ -596,7 +596,7 @@ let rec reflexivity_with_destruct_cases g =
 	 match sc with
 	     None -> tclIDTAC g
 	   | Some id ->
-	       match kind_of_term  (pf_unsafe_type_of g (mkVar id)) with
+	       match kind_of_term  (pf_unsafe_type_of g (EConstr.mkVar id)) with
 		 | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind ->
 		     if Equality.discriminable (pf_env g) (project g) t1 t2
 		     then Proofview.V82.of_tactic (Equality.discrHyp id) g
@@ -661,7 +661,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     (* We get the constant and the principle corresponding to this lemma *)
     let f = funcs.(i) in
     let graph_principle = nf_zeta (EConstr.of_constr schemes.(i))  in
-    let princ_type = pf_unsafe_type_of g graph_principle in
+    let princ_type = pf_unsafe_type_of g (EConstr.of_constr graph_principle) in
     let princ_infos = Tactics.compute_elim_sig princ_type in
     (* Then we get the number of argument of the function
        and compute a fresh name for each of them
@@ -919,7 +919,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
    if the type of hypothesis has not this form or if we cannot find the completeness lemma then we do nothing
 *)
 let revert_graph kn post_tac hid g =
-    let typ = pf_unsafe_type_of g (mkVar hid) in
+    let typ = pf_unsafe_type_of g (EConstr.mkVar hid) in
     match kind_of_term typ with
       | App(i,args) when isInd i ->
 	  let ((kn',num) as ind'),u = destInd i in
@@ -970,7 +970,7 @@ let revert_graph kn post_tac hid g =
 let functional_inversion kn hid fconst f_correct : tactic =
   fun g ->
     let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps g) Id.Set.empty in
-    let type_of_h = pf_unsafe_type_of g (mkVar hid) in
+    let type_of_h = pf_unsafe_type_of g (EConstr.mkVar hid) in
     match kind_of_term type_of_h with
       | App(eq,args) when eq_constr eq (make_eq ())  ->
 	  let pre_tac,f_args,res =
@@ -1022,7 +1022,7 @@ let invfun qhyp f g =
        Proofview.V82.of_tactic begin
 	Tactics.try_intros_until
 	  (fun hid -> Proofview.V82.tactic begin fun g ->
-	     let hyp_typ = pf_unsafe_type_of g (mkVar hid)  in
+	     let hyp_typ = pf_unsafe_type_of g (EConstr.mkVar hid)  in
 	     match kind_of_term hyp_typ with
 	       | App(eq,args) when eq_constr eq (make_eq ()) ->
 		   begin
-- 
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/funind/invfun.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 6359255626..b2419b1a5d 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -598,9 +598,9 @@ let rec reflexivity_with_destruct_cases g =
 	   | Some id ->
 	       match kind_of_term  (pf_unsafe_type_of g (EConstr.mkVar id)) with
 		 | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind ->
-		     if Equality.discriminable (pf_env g) (project g) t1 t2
+		     if Equality.discriminable (pf_env g) (project g) (EConstr.of_constr t1) (EConstr.of_constr t2)
 		     then Proofview.V82.of_tactic (Equality.discrHyp id) g
-		     else if Equality.injectable (pf_env g) (project g) t1 t2
+		     else if Equality.injectable (pf_env g) (project g) (EConstr.of_constr t1) (EConstr.of_constr t2)
 		     then tclTHENSEQ [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite]  g
 		     else tclIDTAC g
 		 | _ -> tclIDTAC g
-- 
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/funind/invfun.ml | 44 +++++++++++++++++++++++---------------------
 1 file changed, 23 insertions(+), 21 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index b2419b1a5d..36fb6dad3d 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -252,7 +252,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
     (* and the principle to use in this lemma in $\zeta$ normal form *)
     let f_principle,princ_type = schemes.(i) in
     let princ_type =  nf_zeta (EConstr.of_constr princ_type) in
-    let princ_infos = Tactics.compute_elim_sig princ_type in
+    let princ_type = EConstr.of_constr princ_type in
+    let princ_infos = Tactics.compute_elim_sig evd princ_type in
     (* The number of args of the function is then easily computable *)
     let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in
     let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
@@ -315,7 +316,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 			     match kind_of_term t'',kind_of_term t''' with
 			       | App(eq,args), App(graph',_)
 				   when
-				     (eq_constr eq eq_ind) &&
+				     (Term.eq_constr eq eq_ind) &&
 				       Array.exists  (Constr.eq_constr_nounivs graph') graphs_constr ->
 				   (args.(2)::(mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|]))
 				    ::acc)
@@ -387,7 +388,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
 	    (* Conclusion *)
 	    observe_tac "exact" (fun g ->
-				 Proofview.V82.of_tactic (exact_check (app_constructor g)) g)  
+				 Proofview.V82.of_tactic (exact_check (EConstr.of_constr (app_constructor g))) g)  
 	  ]
       )
 	g
@@ -440,7 +441,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	observe_tac "principle" (Proofview.V82.of_tactic (assert_by
 	  (Name principle_id)
 	  princ_type
-	  (exact_check f_principle)));
+	  (exact_check (EConstr.of_constr f_principle))));
 	observe_tac "intro args_names" (tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) args_names);
 	(* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty  ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
 	observe_tac "idtac" tclIDTAC;
@@ -450,7 +451,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	       (fun gl ->
 		let term = mkApp (mkVar principle_id,Array.of_list bindings) in
 		let gl', _ty = pf_eapply (Typing.type_of ~refresh:true)  gl (EConstr.of_constr term) in
-		Proofview.V82.of_tactic (apply term) gl')
+		Proofview.V82.of_tactic (apply (EConstr.of_constr term)) gl')
 	   ))
 	  (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
       ]
@@ -467,7 +468,7 @@ let generalize_dependent_of x hyp g =
   tclMAP
     (function
        | LocalAssum (id,t) when not (Id.equal id hyp) &&
-	   (Termops.occur_var (pf_env g) (project g) x (EConstr.of_constr t)) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
+	   (Termops.occur_var (pf_env g) (project g) x (EConstr.of_constr t)) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [EConstr.mkVar id])) (thin [id])
        | _ -> tclIDTAC
     )
     (pf_hyps g)
@@ -495,7 +496,7 @@ and intros_with_rewrite_aux : tactic =
 	  | Prod(_,t,t') ->
 	      begin
 		match kind_of_term t with
-		  | App(eq,args) when (eq_constr eq eq_ind)  ->
+		  | App(eq,args) when (Term.eq_constr eq eq_ind)  ->
  		      if Reductionops.is_conv (pf_env g) (project g) (EConstr.of_constr args.(1)) (EConstr.of_constr args.(2))
 		      then
 			let id = pf_get_new_id (Id.of_string "y") g  in
@@ -541,11 +542,11 @@ and intros_with_rewrite_aux : tactic =
 			    intros_with_rewrite
 			  ] g
 			end
-		  | Ind _ when eq_constr t (Coqlib.build_coq_False ()) ->
+		  | Ind _ when Term.eq_constr t (Coqlib.build_coq_False ()) ->
 		      Proofview.V82.of_tactic tauto g
 		  | Case(_,_,v,_) ->
 		      tclTHENSEQ[
-			Proofview.V82.of_tactic (simplest_case v);
+			Proofview.V82.of_tactic (simplest_case (EConstr.of_constr v));
 			intros_with_rewrite
 		      ] g
 		  | LetIn _ ->
@@ -582,7 +583,7 @@ let rec reflexivity_with_destruct_cases g =
       match kind_of_term (snd (destApp (pf_concl g))).(2) with
 	| Case(_,_,v,_) ->
 	    tclTHENSEQ[
-	      Proofview.V82.of_tactic (simplest_case v);
+	      Proofview.V82.of_tactic (simplest_case (EConstr.of_constr v));
 	      Proofview.V82.of_tactic intros;
 	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
 	    ]
@@ -597,7 +598,7 @@ let rec reflexivity_with_destruct_cases g =
 	     None -> tclIDTAC g
 	   | Some id ->
 	       match kind_of_term  (pf_unsafe_type_of g (EConstr.mkVar id)) with
-		 | App(eq,[|_;t1;t2|]) when eq_constr eq eq_ind ->
+		 | App(eq,[|_;t1;t2|]) when Term.eq_constr eq eq_ind ->
 		     if Equality.discriminable (pf_env g) (project g) (EConstr.of_constr t1) (EConstr.of_constr t2)
 		     then Proofview.V82.of_tactic (Equality.discrHyp id) g
 		     else if Equality.injectable (pf_env g) (project g) (EConstr.of_constr t1) (EConstr.of_constr t2)
@@ -662,7 +663,8 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     let f = funcs.(i) in
     let graph_principle = nf_zeta (EConstr.of_constr schemes.(i))  in
     let princ_type = pf_unsafe_type_of g (EConstr.of_constr graph_principle) in
-    let princ_infos = Tactics.compute_elim_sig princ_type in
+    let princ_type = EConstr.of_constr princ_type in
+    let princ_infos = Tactics.compute_elim_sig (project g) princ_type in
     (* Then we get the number of argument of the function
        and compute a fresh name for each of them
     *)
@@ -717,7 +719,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	       })
 	    Locusops.onConcl)
 	  ;
-	  Proofview.V82.of_tactic (generalize (List.map mkVar ids));
+	  Proofview.V82.of_tactic (generalize (List.map EConstr.mkVar ids));
 	  thin ids
 	]
       else
@@ -756,10 +758,10 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     tclTHENSEQ
       [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]);
 	observe_tac "h_generalize"
-	(Proofview.V82.of_tactic (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]));
+	(Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas))]));
 	Proofview.V82.of_tactic (Simple.intro graph_principle_id);
 	observe_tac "" (tclTHEN_i
-	  (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
+	  (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (EConstr.mkVar hres,NoBindings) (Some (EConstr.mkVar graph_principle_id,NoBindings)))))
 	  (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
       ]
       g
@@ -939,7 +941,7 @@ let revert_graph kn post_tac hid g =
 		  let f_args,res = Array.chop (Array.length args - 1) args in
 		  tclTHENSEQ
 		    [
-		      Proofview.V82.of_tactic (generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]);
+		      Proofview.V82.of_tactic (generalize [EConstr.of_constr (applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid]))]);
 		      thin [hid];
 		      Proofview.V82.of_tactic (Simple.intro hid);
 		      post_tac hid
@@ -972,18 +974,18 @@ let functional_inversion kn hid fconst f_correct : tactic =
     let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps g) Id.Set.empty in
     let type_of_h = pf_unsafe_type_of g (EConstr.mkVar hid) in
     match kind_of_term type_of_h with
-      | App(eq,args) when eq_constr eq (make_eq ())  ->
+      | App(eq,args) when Term.eq_constr eq (make_eq ())  ->
 	  let pre_tac,f_args,res =
 	    match kind_of_term args.(1),kind_of_term args.(2) with
-	      | App(f,f_args),_ when eq_constr f fconst ->
+	      | App(f,f_args),_ when Term.eq_constr f fconst ->
 		  ((fun hid -> Proofview.V82.of_tactic (intros_symmetry (Locusops.onHyp hid))),f_args,args.(2))
-	      |_,App(f,f_args) when eq_constr f fconst ->
+	      |_,App(f,f_args) when Term.eq_constr f fconst ->
 		 ((fun hid -> tclIDTAC),f_args,args.(1))
 	      | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2)
 	  in
 	  tclTHENSEQ[
 	    pre_tac hid;
-	    Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]);
+	    Proofview.V82.of_tactic (generalize [EConstr.of_constr (applist(f_correct,(Array.to_list f_args)@[res;mkVar hid]))]);
 	    thin [hid];
 	    Proofview.V82.of_tactic (Simple.intro hid);
 	    Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid));
@@ -1024,7 +1026,7 @@ let invfun qhyp f g =
 	  (fun hid -> Proofview.V82.tactic begin fun g ->
 	     let hyp_typ = pf_unsafe_type_of g (EConstr.mkVar hid)  in
 	     match kind_of_term hyp_typ with
-	       | App(eq,args) when eq_constr eq (make_eq ()) ->
+	       | App(eq,args) when Term.eq_constr eq (make_eq ()) ->
 		   begin
 		     let f1,_ = decompose_app args.(1) in
 		     try
-- 
cgit v1.2.3


From 3f9e56fcbf479999325a86bbdaeefd6a0be13c65 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 18 Nov 2016 20:35:01 +0100
Subject: Equality API using EConstr.

---
 plugins/funind/invfun.ml | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 36fb6dad3d..d29d4694f3 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -385,7 +385,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	    (* introducing the the result of the graph and the equality hypothesis *)
 	    observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]);
 	    (* replacing [res] with its value *)
-	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
+	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar hres)));
 	    (* Conclusion *)
 	    observe_tac "exact" (fun g ->
 				 Proofview.V82.of_tactic (exact_check (EConstr.of_constr (app_constructor g))) g)  
@@ -520,7 +520,7 @@ and intros_with_rewrite_aux : tactic =
 			let id = pf_get_new_id (Id.of_string "y") g  in
 			tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id);
 				     generalize_dependent_of (destVar args.(1)) id;
-				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
+				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar id)));
 				     intros_with_rewrite
 				   ]
 			  g
@@ -529,7 +529,7 @@ and intros_with_rewrite_aux : tactic =
 			let id = pf_get_new_id (Id.of_string "y") g  in
 			tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id);
 				     generalize_dependent_of (destVar args.(2)) id;
-				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id)));
+				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (EConstr.mkVar id)));
 				     intros_with_rewrite
 				   ]
 			  g
@@ -538,7 +538,7 @@ and intros_with_rewrite_aux : tactic =
 			  let id = pf_get_new_id (Id.of_string "y") g  in
 			  tclTHENSEQ[
 			    Proofview.V82.of_tactic (Simple.intro id);
-			    tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
+			    tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar id)));
 			    intros_with_rewrite
 			  ] g
 			end
@@ -709,7 +709,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	in
 	tclTHENSEQ[
 	  tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids;
-	  Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma));
+	  Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.of_constr (mkConst eq_lemma)));
 	  (* Don't forget to $\zeta$ normlize the term since the principles
              have been $\zeta$-normalized *)
 	  Proofview.V82.of_tactic (reduce
-- 
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/funind/invfun.ml | 12 +++++++-----
 1 file changed, 7 insertions(+), 5 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index d29d4694f3..c02b64c1f5 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -252,7 +252,6 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
     (* and the principle to use in this lemma in $\zeta$ normal form *)
     let f_principle,princ_type = schemes.(i) in
     let princ_type =  nf_zeta (EConstr.of_constr princ_type) in
-    let princ_type = EConstr.of_constr princ_type in
     let princ_infos = Tactics.compute_elim_sig evd princ_type in
     (* The number of args of the function is then easily computable *)
     let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in
@@ -429,7 +428,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) decl p ->
 	     let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in
-	     (nf_zeta (EConstr.of_constr p))::bindings,id::avoid)
+	     (EConstr.Unsafe.to_constr (nf_zeta (EConstr.of_constr p)))::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
 	  (lemmas)))
@@ -662,7 +661,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     (* We get the constant and the principle corresponding to this lemma *)
     let f = funcs.(i) in
     let graph_principle = nf_zeta (EConstr.of_constr schemes.(i))  in
-    let princ_type = pf_unsafe_type_of g (EConstr.of_constr graph_principle) in
+    let princ_type = pf_unsafe_type_of g graph_principle in
     let princ_type = EConstr.of_constr princ_type in
     let princ_infos = Tactics.compute_elim_sig (project g) princ_type in
     (* Then we get the number of argument of the function
@@ -754,14 +753,15 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	g
     in
     let params_names = fst (List.chop princ_infos.nparams args_names) in
+    let open EConstr in
     let params = List.map mkVar params_names in
     tclTHENSEQ
       [ tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) (args_names@[res;hres]);
 	observe_tac "h_generalize"
-	(Proofview.V82.of_tactic (generalize [EConstr.of_constr (mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas))]));
+	(Proofview.V82.of_tactic (generalize [mkApp(applist(graph_principle,params),Array.map (fun c -> applist(c,params)) lemmas)]));
 	Proofview.V82.of_tactic (Simple.intro graph_principle_id);
 	observe_tac "" (tclTHEN_i
-	  (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (EConstr.mkVar hres,NoBindings) (Some (EConstr.mkVar graph_principle_id,NoBindings)))))
+	  (observe_tac "elim" (Proofview.V82.of_tactic (elim false None (mkVar hres,NoBindings) (Some (mkVar graph_principle_id,NoBindings)))))
 	  (fun i g -> observe_tac "prove_branche" (prove_branche i) g ))
       ]
       g
@@ -796,6 +796,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
 	 let _ = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr type_of_lemma) in 
 	   let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
+	   let type_of_lemma = EConstr.Unsafe.to_constr type_of_lemma in
 	   observe (str "type_of_lemma := " ++ Printer.pr_lconstr_env (Global.env ()) !evd type_of_lemma);
 	   type_of_lemma,type_info
 	)
@@ -863,6 +864,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	   Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
 	 in
 	 let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
+	 let type_of_lemma = EConstr.Unsafe.to_constr type_of_lemma in
 	 observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma);
 	 type_of_lemma,type_info
 	)
-- 
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/funind/invfun.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index c02b64c1f5..ca066c4cca 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -399,8 +399,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	   match ctxt with
 	     | [] | [_] | [_;_] -> anomaly (Pp.str "bad context")
 	     | hres::res::decl::ctxt ->
-		let res = Termops.it_mkLambda_or_LetIn
-			    (Termops.it_mkProd_or_LetIn concl [hres;res])
+		let res = Term.it_mkLambda_or_LetIn
+			    (Term.it_mkProd_or_LetIn concl [hres;res])
 			    (LocalAssum (RelDecl.get_name decl, RelDecl.get_type decl) :: ctxt)
 		in
 		res
@@ -793,7 +793,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 in
 	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
 	 graphs_constr.(i) <- graph;
-	 let type_of_lemma = Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
+	 let type_of_lemma = Term.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
 	 let _ = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr type_of_lemma) in 
 	   let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
 	   let type_of_lemma = EConstr.Unsafe.to_constr type_of_lemma in
@@ -861,7 +861,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
 	 graphs_constr.(i) <- graph;
 	 let type_of_lemma =
-	   Termops.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
+	   Term.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
 	 in
 	 let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
 	 let type_of_lemma = EConstr.Unsafe.to_constr type_of_lemma in
-- 
cgit v1.2.3


From 531590c223af42c07a93142ab0cea470a98964e6 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Thu, 24 Nov 2016 17:15:15 +0100
Subject: Removing compatibility layers in Retyping

---
 plugins/funind/invfun.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index ca066c4cca..27528c2dcc 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -135,6 +135,7 @@ let generate_type evd g_to_f f graph i =
   in
   evd:=evd';
   let graph_arity = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr graph) in
+  let graph_arity = EConstr.Unsafe.to_constr graph_arity in
   let ctxt,_ = decompose_prod_assum graph_arity in
   let fun_ctxt,res_type =
     match ctxt with
@@ -203,6 +204,7 @@ let find_induction_principle evd f =
     | Some rect_lemma ->
        let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (Globnames.ConstRef rect_lemma) in
        let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr rect_lemma) in
+       let typ = EConstr.Unsafe.to_constr typ in
        evd:=evd';
        rect_lemma,typ
 
-- 
cgit v1.2.3


From a5499688bd76def8de3d8e1089a49c7a08430903 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Fri, 25 Nov 2016 14:54:40 +0100
Subject: Funind API using EConstr.

---
 plugins/funind/invfun.ml | 212 +++++++++++++++++++++++++----------------------
 1 file changed, 114 insertions(+), 98 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 27528c2dcc..be82010d9d 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -12,6 +12,7 @@ open CErrors
 open Util
 open Names
 open Term
+open EConstr
 open Vars
 open Pp
 open Globnames
@@ -25,6 +26,12 @@ open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
 
+let local_assum (na, t) =
+  RelDecl.LocalAssum (na, EConstr.Unsafe.to_constr t)
+
+let local_def (na, b, t) =
+  RelDecl.LocalDef (na, EConstr.Unsafe.to_constr b, EConstr.Unsafe.to_constr t)
+
 (* Some pretty printing function for debugging purpose *)
 
 let pr_binding prc  =
@@ -108,11 +115,11 @@ let thin ids gl = Proofview.V82.of_tactic (Tactics.clear ids) gl
 
 let make_eq () =
   try
-    Universes.constr_of_global (Coqlib.build_coq_eq ())
+    EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq ()))
   with _ -> assert false 
 let make_eq_refl () =
   try
-    Universes.constr_of_global (Coqlib.build_coq_eq_refl ())
+    EConstr.of_constr (Universes.constr_of_global (Coqlib.build_coq_eq_refl ()))
   with _ -> assert false
 
 	  
@@ -131,16 +138,16 @@ let make_eq_refl () =
 let generate_type evd g_to_f f graph i =
   (*i we deduce the number of arguments of the function and its returned type from the graph i*)
   let evd',graph =
-    Evd.fresh_global  (Global.env ()) !evd  (Globnames.IndRef (fst (destInd graph)))
+    Evd.fresh_global  (Global.env ()) !evd  (Globnames.IndRef (fst (destInd !evd graph)))
   in
+  let graph = EConstr.of_constr graph in
   evd:=evd';
-  let graph_arity = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr graph) in
-  let graph_arity = EConstr.Unsafe.to_constr graph_arity in
-  let ctxt,_ = decompose_prod_assum graph_arity in
+  let graph_arity = Typing.e_type_of (Global.env ()) evd graph in
+  let ctxt,_ = decompose_prod_assum !evd graph_arity in
   let fun_ctxt,res_type =
     match ctxt with
       | [] | [_] -> anomaly (Pp.str "Not a valid context")
-      | decl :: fun_ctxt -> fun_ctxt, RelDecl.get_type decl
+      | decl :: fun_ctxt -> fun_ctxt, EConstr.of_constr (RelDecl.get_type decl)
   in
   let rec args_from_decl i accu = function
   | [] -> accu
@@ -180,12 +187,12 @@ let generate_type evd g_to_f f graph i =
     \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res,  \]
     i*)
   let pre_ctxt =
-    LocalAssum (Name res_id, lift 1 res_type) :: LocalDef (Name fv_id, mkApp (f,args_as_rels), res_type) :: fun_ctxt
+    local_assum (Name res_id, lift 1 res_type) :: local_def (Name fv_id, mkApp (f,args_as_rels), res_type) :: fun_ctxt
   in
   (*i and we can return the solution depending on which lemma type we are defining i*)
   if g_to_f
-  then LocalAssum (Anonymous,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph
-  else LocalAssum (Anonymous,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph
+  then local_assum (Anonymous,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph
+  else local_assum (Anonymous,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph
 
 
 (*
@@ -194,7 +201,7 @@ let generate_type evd g_to_f f graph i =
    WARNING: while convertible, [type_of body] and [type] can be non equal
 *)
 let find_induction_principle evd f =
-  let f_as_constant,u =  match kind_of_term f with
+  let f_as_constant,u =  match EConstr.kind !evd f with
     | Const c' -> c'
     | _ -> error "Must be used with a function"
   in
@@ -203,8 +210,8 @@ let find_induction_principle evd f =
     | None -> raise Not_found
     | Some rect_lemma ->
        let evd',rect_lemma = Evd.fresh_global  (Global.env ()) !evd  (Globnames.ConstRef rect_lemma) in
-       let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' (EConstr.of_constr rect_lemma) in
-       let typ = EConstr.Unsafe.to_constr typ in
+       let rect_lemma = EConstr.of_constr rect_lemma in
+       let evd',typ = Typing.type_of ~refresh:true (Global.env ()) evd' rect_lemma in
        evd:=evd';
        rect_lemma,typ
 
@@ -248,12 +255,12 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
        \[fun (x_1:t_1)\ldots(x_n:t_n)=> fun  fv => fun res => res = fv \rightarrow graph\ x_1\ldots x_n\ res\]
     *)
     (* we the get the definition of the graphs block *)
-    let graph_ind,u = destInd graphs_constr.(i) in
+    let graph_ind,u = destInd evd graphs_constr.(i) in
     let kn = fst graph_ind in
     let mib,_ = Global.lookup_inductive graph_ind in
     (* and the principle to use in this lemma in $\zeta$ normal form *)
     let f_principle,princ_type = schemes.(i) in
-    let princ_type =  nf_zeta (EConstr.of_constr princ_type) in
+    let princ_type =  nf_zeta princ_type in
     let princ_infos = Tactics.compute_elim_sig evd princ_type in
     (* The number of args of the function is then easily computable *)
     let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in
@@ -273,13 +280,13 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	(fun decl ->
 	   List.map
 	     (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id))
-	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum (RelDecl.get_type decl)))))
+	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (EConstr.of_constr (RelDecl.get_type decl))))))
 	)
 	branches
     in
     (* before building the full intro pattern for the principle *)
     let eq_ind = make_eq () in
-    let eq_construct = mkConstructUi (destInd eq_ind, 1) in
+    let eq_construct = mkConstructUi (destInd evd eq_ind, 1) in
     (* The next to referencies will be used to find out which constructor to apply in each branch *)
     let ind_number = ref 0
     and min_constr_number = ref 0 in
@@ -307,18 +314,20 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
       let constructor_args g =
 	List.fold_right 
 	  (fun hid acc ->
-	     let type_of_hid = pf_unsafe_type_of g (EConstr.mkVar hid) in
-	     match kind_of_term type_of_hid with
+	     let type_of_hid = pf_unsafe_type_of g (mkVar hid) in
+	     let type_of_hid = EConstr.of_constr type_of_hid in
+	     let sigma = project g in
+	     match EConstr.kind sigma type_of_hid with
 	       | Prod(_,_,t') ->
 		   begin
-		     match kind_of_term t' with
+		     match EConstr.kind sigma t' with
 		       | Prod(_,t'',t''') ->
 			   begin
-			     match kind_of_term t'',kind_of_term t''' with
+			     match EConstr.kind sigma t'',EConstr.kind sigma t''' with
 			       | App(eq,args), App(graph',_)
 				   when
-				     (Term.eq_constr eq eq_ind) &&
-				       Array.exists  (Constr.eq_constr_nounivs graph') graphs_constr ->
+				     (EConstr.eq_constr sigma eq eq_ind) &&
+				       Array.exists  (EConstr.eq_constr_nounivs sigma graph') graphs_constr ->
 				   (args.(2)::(mkApp(mkVar hid,[|args.(2);(mkApp(eq_construct,[|args.(0);args.(2)|]))|]))
 				    ::acc)
 			       | _ -> mkVar hid ::  acc
@@ -386,10 +395,10 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	    (* introducing the the result of the graph and the equality hypothesis *)
 	    observe_tac "introducing" (tclMAP (fun x -> Proofview.V82.of_tactic (Simple.intro x)) [res;hres]);
 	    (* replacing [res] with its value *)
-	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar hres)));
+	    observe_tac "rewriting res value" (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar hres)));
 	    (* Conclusion *)
 	    observe_tac "exact" (fun g ->
-				 Proofview.V82.of_tactic (exact_check (EConstr.of_constr (app_constructor g))) g)  
+				 Proofview.V82.of_tactic (exact_check (app_constructor g)) g)  
 	  ]
       )
 	g
@@ -401,8 +410,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	   match ctxt with
 	     | [] | [_] | [_;_] -> anomaly (Pp.str "bad context")
 	     | hres::res::decl::ctxt ->
-		let res = Term.it_mkLambda_or_LetIn
-			    (Term.it_mkProd_or_LetIn concl [hres;res])
+		let res = EConstr.it_mkLambda_or_LetIn
+			    (EConstr.it_mkProd_or_LetIn concl [hres;res])
 			    (LocalAssum (RelDecl.get_name decl, RelDecl.get_type decl) :: ctxt)
 		in
 		res
@@ -430,7 +439,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	List.rev (fst  (List.fold_left2
 	  (fun (bindings,avoid) decl p ->
 	     let id = Namegen.next_ident_away (Nameops.out_name (RelDecl.get_name decl)) avoid in
-	     (EConstr.Unsafe.to_constr (nf_zeta (EConstr.of_constr p)))::bindings,id::avoid)
+	     (nf_zeta p)::bindings,id::avoid)
 	  ([],avoid)
 	  princ_infos.predicates
 	  (lemmas)))
@@ -442,7 +451,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	observe_tac "principle" (Proofview.V82.of_tactic (assert_by
 	  (Name principle_id)
 	  princ_type
-	  (exact_check (EConstr.of_constr f_principle))));
+	  (exact_check f_principle)));
 	observe_tac "intro args_names" (tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) args_names);
 	(* observe_tac "titi" (pose_proof (Name (Id.of_string "__")) (Reductionops.nf_beta Evd.empty  ((mkApp (mkVar principle_id,Array.of_list bindings))))); *)
 	observe_tac "idtac" tclIDTAC;
@@ -451,8 +460,8 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	     "functional_induction" (
 	       (fun gl ->
 		let term = mkApp (mkVar principle_id,Array.of_list bindings) in
-		let gl', _ty = pf_eapply (Typing.type_of ~refresh:true)  gl (EConstr.of_constr term) in
-		Proofview.V82.of_tactic (apply (EConstr.of_constr term)) gl')
+		let gl', _ty = pf_eapply (Typing.type_of ~refresh:true)  gl term in
+		Proofview.V82.of_tactic (apply term) gl')
 	   ))
 	  (fun i g -> observe_tac ("proving branche "^string_of_int i) (prove_branche i) g )
       ]
@@ -469,7 +478,7 @@ let generalize_dependent_of x hyp g =
   tclMAP
     (function
        | LocalAssum (id,t) when not (Id.equal id hyp) &&
-	   (Termops.occur_var (pf_env g) (project g) x (EConstr.of_constr t)) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [EConstr.mkVar id])) (thin [id])
+	   (Termops.occur_var (pf_env g) (project g) x (EConstr.of_constr t)) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
        | _ -> tclIDTAC
     )
     (pf_hyps g)
@@ -493,44 +502,45 @@ let  rec intros_with_rewrite g =
 and intros_with_rewrite_aux : tactic =
   fun g ->
     let eq_ind = make_eq () in
-    match kind_of_term (pf_concl g) with
+    let sigma = project g in
+    match EConstr.kind sigma (EConstr.of_constr (pf_concl g)) with
 	  | Prod(_,t,t') ->
 	      begin
-		match kind_of_term t with
-		  | App(eq,args) when (Term.eq_constr eq eq_ind)  ->
- 		      if Reductionops.is_conv (pf_env g) (project g) (EConstr.of_constr args.(1)) (EConstr.of_constr args.(2))
+		match EConstr.kind sigma t with
+		  | App(eq,args) when (EConstr.eq_constr sigma eq eq_ind)  ->
+ 		      if Reductionops.is_conv (pf_env g) (project g) args.(1) args.(2)
 		      then
 			let id = pf_get_new_id (Id.of_string "y") g  in
 			tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id); thin [id]; intros_with_rewrite ] g
-		      else if isVar args.(1) && (Environ.evaluable_named (destVar args.(1)) (pf_env g)) 
+		      else if isVar sigma args.(1) && (Environ.evaluable_named (destVar sigma args.(1)) (pf_env g)) 
 		      then tclTHENSEQ[
-			Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))]);
-			tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(1)))] ((destVar args.(1)),Locus.InHyp) )))
+			Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))]);
+			tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(1)))] ((destVar sigma args.(1)),Locus.InHyp) )))
 			  (pf_ids_of_hyps g);
 			intros_with_rewrite
 		      ] g
-		      else if isVar args.(2) && (Environ.evaluable_named (destVar args.(2)) (pf_env g)) 
+		      else if isVar sigma args.(2) && (Environ.evaluable_named (destVar sigma args.(2)) (pf_env g)) 
 		      then tclTHENSEQ[
-			Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))]);
-			tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar args.(2)))] ((destVar args.(2)),Locus.InHyp) )))
+			Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))]);
+			tclMAP (fun id -> tclTRY(Proofview.V82.of_tactic (unfold_in_hyp [(Locus.AllOccurrences, Names.EvalVarRef (destVar sigma args.(2)))] ((destVar sigma args.(2)),Locus.InHyp) )))
 			  (pf_ids_of_hyps g);
 			intros_with_rewrite
 		      ] g
-		      else if isVar args.(1)
+		      else if isVar sigma args.(1)
 		      then
 			let id = pf_get_new_id (Id.of_string "y") g  in
 			tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id);
-				     generalize_dependent_of (destVar args.(1)) id;
-				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar id)));
+				     generalize_dependent_of (destVar sigma args.(1)) id;
+				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
 				     intros_with_rewrite
 				   ]
 			  g
-		      else if isVar args.(2) 
+		      else if isVar sigma args.(2) 
 		      then 
 			let id = pf_get_new_id (Id.of_string "y") g  in
 			tclTHENSEQ [ Proofview.V82.of_tactic (Simple.intro id);
-				     generalize_dependent_of (destVar args.(2)) id;
-				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (EConstr.mkVar id)));
+				     generalize_dependent_of (destVar sigma args.(2)) id;
+				     tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar id)));
 				     intros_with_rewrite
 				   ]
 			  g
@@ -539,15 +549,15 @@ and intros_with_rewrite_aux : tactic =
 			  let id = pf_get_new_id (Id.of_string "y") g  in
 			  tclTHENSEQ[
 			    Proofview.V82.of_tactic (Simple.intro id);
-			    tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.mkVar id)));
+			    tclTRY (Proofview.V82.of_tactic (Equality.rewriteLR (mkVar id)));
 			    intros_with_rewrite
 			  ] g
 			end
-		  | Ind _ when Term.eq_constr t (Coqlib.build_coq_False ()) ->
+		  | Ind _ when EConstr.eq_constr sigma t (EConstr.of_constr (Coqlib.build_coq_False ())) ->
 		      Proofview.V82.of_tactic tauto g
 		  | Case(_,_,v,_) ->
 		      tclTHENSEQ[
-			Proofview.V82.of_tactic (simplest_case (EConstr.of_constr v));
+			Proofview.V82.of_tactic (simplest_case v);
 			intros_with_rewrite
 		      ] g
 		  | LetIn _ ->
@@ -581,10 +591,10 @@ and intros_with_rewrite_aux : tactic =
 let rec reflexivity_with_destruct_cases g =
   let destruct_case () =
     try
-      match kind_of_term (snd (destApp (pf_concl g))).(2) with
+      match EConstr.kind (project g) (snd (destApp (project g) (EConstr.of_constr (pf_concl g)))).(2) with
 	| Case(_,_,v,_) ->
 	    tclTHENSEQ[
-	      Proofview.V82.of_tactic (simplest_case (EConstr.of_constr v));
+	      Proofview.V82.of_tactic (simplest_case v);
 	      Proofview.V82.of_tactic intros;
 	      observe_tac "reflexivity_with_destruct_cases" reflexivity_with_destruct_cases
 	    ]
@@ -598,11 +608,11 @@ let rec reflexivity_with_destruct_cases g =
 	 match sc with
 	     None -> tclIDTAC g
 	   | Some id ->
-	       match kind_of_term  (pf_unsafe_type_of g (EConstr.mkVar id)) with
-		 | App(eq,[|_;t1;t2|]) when Term.eq_constr eq eq_ind ->
-		     if Equality.discriminable (pf_env g) (project g) (EConstr.of_constr t1) (EConstr.of_constr t2)
+	       match EConstr.kind (project g) (EConstr.of_constr (pf_unsafe_type_of g (mkVar id))) with
+		 | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind ->
+		     if Equality.discriminable (pf_env g) (project g) t1 t2
 		     then Proofview.V82.of_tactic (Equality.discrHyp id) g
-		     else if Equality.injectable (pf_env g) (project g) (EConstr.of_constr t1) (EConstr.of_constr t2)
+		     else if Equality.injectable (pf_env g) (project g) t1 t2
 		     then tclTHENSEQ [Proofview.V82.of_tactic (Equality.injHyp None id);thin [id];intros_with_rewrite]  g
 		     else tclIDTAC g
 		 | _ -> tclIDTAC g
@@ -657,7 +667,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     *)
     let lemmas =
       Array.map
-	(fun (_,(ctxt,concl)) -> nf_zeta (EConstr.of_constr (Termops.it_mkLambda_or_LetIn concl ctxt)))
+	(fun (_,(ctxt,concl)) -> nf_zeta (EConstr.it_mkLambda_or_LetIn concl ctxt))
 	lemmas_types_infos
     in
     (* We get the constant and the principle corresponding to this lemma *)
@@ -698,7 +708,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     let rewrite_tac j ids : tactic =
       let graph_def = graphs.(j) in
       let infos =
-        try find_Function_infos (fst (destConst funcs.(j)))
+        try find_Function_infos (fst (destConst (project g) funcs.(j)))
         with Not_found ->  error "No graph found"
       in
       if infos.is_general
@@ -710,7 +720,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	in
 	tclTHENSEQ[
 	  tclMAP (fun id -> Proofview.V82.of_tactic (Simple.intro id)) ids;
-	  Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.of_constr (mkConst eq_lemma)));
+	  Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_lemma));
 	  (* Don't forget to $\zeta$ normlize the term since the principles
              have been $\zeta$-normalized *)
 	  Proofview.V82.of_tactic (reduce
@@ -720,11 +730,11 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	       })
 	    Locusops.onConcl)
 	  ;
-	  Proofview.V82.of_tactic (generalize (List.map EConstr.mkVar ids));
+	  Proofview.V82.of_tactic (generalize (List.map mkVar ids));
 	  thin ids
 	]
       else
-        Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst f)))])
+        Proofview.V82.of_tactic (unfold_in_concl [(Locus.AllOccurrences, Names.EvalConstRef (fst (destConst (project g) f)))])
     in
     (* The proof of each branche itself *)
     let ind_number = ref 0 in
@@ -795,11 +805,10 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 in
 	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
 	 graphs_constr.(i) <- graph;
-	 let type_of_lemma = Term.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
-	 let _ = Typing.e_type_of (Global.env ()) evd (EConstr.of_constr type_of_lemma) in 
-	   let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
-	   let type_of_lemma = EConstr.Unsafe.to_constr type_of_lemma in
-	   observe (str "type_of_lemma := " ++ Printer.pr_lconstr_env (Global.env ()) !evd type_of_lemma);
+	 let type_of_lemma = EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt in
+	 let _ = Typing.e_type_of (Global.env ()) evd type_of_lemma in 
+	   let type_of_lemma = nf_zeta type_of_lemma in
+	   observe (str "type_of_lemma := " ++ Printer.pr_leconstr_env (Global.env ()) !evd type_of_lemma);
 	   type_of_lemma,type_info
 	)
 	funs_constr
@@ -818,7 +827,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	  Array.of_list
 	    (List.map
 	       (fun entry ->
-		  (fst (fst(Future.force entry.Entries.const_entry_body)), Option.get entry.Entries.const_entry_type )
+		  (EConstr.of_constr (fst (fst(Future.force entry.Entries.const_entry_body))), EConstr.of_constr (Option.get entry.Entries.const_entry_type ))
 	       )
 	       (make_scheme evd (Array.map_to_list (fun const -> const,GType []) funs))
 	    )
@@ -839,7 +848,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	   lem_id
 	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),((Decl_kinds.Proof Decl_kinds.Theorem)))
            !evd
-	   typ
+	   (EConstr.Unsafe.to_constr typ)
            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
 		   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
@@ -849,7 +858,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 (* let lem_cst = fst (destConst (Constrintern.global_reference lem_id)) in *)
 	 let _,lem_cst_constr = Evd.fresh_global
 				  (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
-	 let (lem_cst,_) = destConst lem_cst_constr in
+        let lem_cst_constr = EConstr.of_constr lem_cst_constr in
+	 let (lem_cst,_) = destConst !evd lem_cst_constr in
 	 update_Function {finfo with correctness_lemma = Some lem_cst};
 
       )
@@ -863,18 +873,17 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let type_info = (type_of_lemma_ctxt,type_of_lemma_concl) in
 	 graphs_constr.(i) <- graph;
 	 let type_of_lemma =
-	   Term.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
+	   EConstr.it_mkProd_or_LetIn type_of_lemma_concl type_of_lemma_ctxt
 	 in
-	 let type_of_lemma = nf_zeta (EConstr.of_constr type_of_lemma) in
-	 let type_of_lemma = EConstr.Unsafe.to_constr type_of_lemma in
-	 observe (str "type_of_lemma := " ++ Printer.pr_lconstr type_of_lemma);
+	 let type_of_lemma = nf_zeta type_of_lemma in
+	 observe (str "type_of_lemma := " ++ Printer.pr_leconstr type_of_lemma);
 	 type_of_lemma,type_info
 	)
 	funs_constr
 	graphs_constr
     in
 
-    let (kn,_) as graph_ind,u  = (destInd graphs_constr.(0)) in
+    let (kn,_) as graph_ind,u  = (destInd !evd graphs_constr.(0)) in
     let mib,mip = Global.lookup_inductive graph_ind in
     let sigma, scheme = 
 	(Indrec.build_mutual_induction_scheme (Global.env ()) !evd
@@ -901,7 +910,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let lem_id = mk_complete_id f_id in
 	 Lemmas.start_proof lem_id
 	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
-	 (fst lemmas_types_infos.(i))
+	 (EConstr.Unsafe.to_constr (fst lemmas_types_infos.(i)))
            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
@@ -910,7 +919,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let finfo = find_Function_infos (fst f_as_constant) in
 	 let _,lem_cst_constr = Evd.fresh_global
 				  (Global.env ()) !evd (Constrintern.locate_reference (Libnames.qualid_of_ident lem_id)) in
-	 let (lem_cst,_) = destConst lem_cst_constr in
+         let lem_cst_constr = EConstr.of_constr lem_cst_constr in
+	 let (lem_cst,_) = destConst !evd lem_cst_constr in
 	 update_Function {finfo with completeness_lemma = Some lem_cst}
       )
       funs)
@@ -925,10 +935,12 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
    if the type of hypothesis has not this form or if we cannot find the completeness lemma then we do nothing
 *)
 let revert_graph kn post_tac hid g =
-    let typ = pf_unsafe_type_of g (EConstr.mkVar hid) in
-    match kind_of_term typ with
-      | App(i,args) when isInd i ->
-	  let ((kn',num) as ind'),u = destInd i in
+    let sigma = project g in
+    let typ = pf_unsafe_type_of g (mkVar hid) in
+    let typ = EConstr.of_constr typ in
+    match EConstr.kind sigma typ with
+      | App(i,args) when isInd sigma i ->
+	  let ((kn',num) as ind'),u = destInd sigma i in
 	  if MutInd.equal kn kn'
 	  then (* We have generated a graph hypothesis so that we must change it if we can *)
 	    let info =
@@ -945,7 +957,7 @@ let revert_graph kn post_tac hid g =
 		  let f_args,res = Array.chop (Array.length args - 1) args in
 		  tclTHENSEQ
 		    [
-		      Proofview.V82.of_tactic (generalize [EConstr.of_constr (applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid]))]);
+		      Proofview.V82.of_tactic (generalize [applist(mkConst f_complete,(Array.to_list f_args)@[res.(0);mkVar hid])]);
 		      thin [hid];
 		      Proofview.V82.of_tactic (Simple.intro hid);
 		      post_tac hid
@@ -976,20 +988,22 @@ let revert_graph kn post_tac hid g =
 let functional_inversion kn hid fconst f_correct : tactic =
   fun g ->
     let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps g) Id.Set.empty in
-    let type_of_h = pf_unsafe_type_of g (EConstr.mkVar hid) in
-    match kind_of_term type_of_h with
-      | App(eq,args) when Term.eq_constr eq (make_eq ())  ->
+    let sigma = project g in
+    let type_of_h = pf_unsafe_type_of g (mkVar hid) in
+    let type_of_h = EConstr.of_constr type_of_h in
+    match EConstr.kind sigma type_of_h with
+      | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ())  ->
 	  let pre_tac,f_args,res =
-	    match kind_of_term args.(1),kind_of_term args.(2) with
-	      | App(f,f_args),_ when Term.eq_constr f fconst ->
+	    match EConstr.kind sigma args.(1),EConstr.kind sigma args.(2) with
+	      | App(f,f_args),_ when EConstr.eq_constr sigma f fconst ->
 		  ((fun hid -> Proofview.V82.of_tactic (intros_symmetry (Locusops.onHyp hid))),f_args,args.(2))
-	      |_,App(f,f_args) when Term.eq_constr f fconst ->
+	      |_,App(f,f_args) when EConstr.eq_constr sigma f fconst ->
 		 ((fun hid -> tclIDTAC),f_args,args.(1))
 	      | _ -> (fun hid -> tclFAIL 1 (mt ())),[||],args.(2)
 	  in
 	  tclTHENSEQ[
 	    pre_tac hid;
-	    Proofview.V82.of_tactic (generalize [EConstr.of_constr (applist(f_correct,(Array.to_list f_args)@[res;mkVar hid]))]);
+	    Proofview.V82.of_tactic (generalize [applist(f_correct,(Array.to_list f_args)@[res;mkVar hid])]);
 	    thin [hid];
 	    Proofview.V82.of_tactic (Simple.intro hid);
 	    Proofview.V82.of_tactic (Inv.inv FullInversion None (NamedHyp hid));
@@ -1028,23 +1042,25 @@ let invfun qhyp f g =
        Proofview.V82.of_tactic begin
 	Tactics.try_intros_until
 	  (fun hid -> Proofview.V82.tactic begin fun g ->
-	     let hyp_typ = pf_unsafe_type_of g (EConstr.mkVar hid)  in
-	     match kind_of_term hyp_typ with
-	       | App(eq,args) when Term.eq_constr eq (make_eq ()) ->
+            let sigma = project g in
+	     let hyp_typ = pf_unsafe_type_of g (mkVar hid)  in
+	     let hyp_typ = EConstr.of_constr hyp_typ in
+	     match EConstr.kind sigma hyp_typ with
+	       | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) ->
 		   begin
-		     let f1,_ = decompose_app args.(1) in
+		     let f1,_ = decompose_app sigma args.(1) in
 		     try
-		       if not (isConst f1) then failwith "";
-		       let finfos = find_Function_infos (fst (destConst f1)) in
+		       if not (isConst sigma f1) then failwith "";
+		       let finfos = find_Function_infos (fst (destConst sigma f1)) in
 		       let f_correct = mkConst(Option.get finfos.correctness_lemma)
 		       and kn = fst finfos.graph_ind
 		       in
 		       functional_inversion kn hid f1 f_correct g
 		     with | Failure "" | Option.IsNone | Not_found ->
 		       try
-			 let f2,_ = decompose_app args.(2) in
-			 if not (isConst f2) then failwith "";
-			 let finfos = find_Function_infos (fst (destConst f2)) in
+			 let f2,_ = decompose_app sigma args.(2) in
+			 if not (isConst sigma f2) then failwith "";
+			 let finfos = find_Function_infos (fst (destConst sigma f2)) in
 			 let f_correct = mkConst(Option.get finfos.correctness_lemma)
 			 and kn = fst finfos.graph_ind
 			 in
-- 
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/funind/invfun.ml | 15 +++++----------
 1 file changed, 5 insertions(+), 10 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index be82010d9d..5cbec77437 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -263,7 +263,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
     let princ_type =  nf_zeta princ_type in
     let princ_infos = Tactics.compute_elim_sig evd princ_type in
     (* The number of args of the function is then easily computable *)
-    let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in
+    let nb_fun_args = nb_prod (project g) (pf_concl g) - 2 in
     let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
     let ids = args_names@(pf_ids_of_hyps g) in
     (* Since we cannot ensure that the functional principle is defined in the
@@ -315,7 +315,6 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	List.fold_right 
 	  (fun hid acc ->
 	     let type_of_hid = pf_unsafe_type_of g (mkVar hid) in
-	     let type_of_hid = EConstr.of_constr type_of_hid in
 	     let sigma = project g in
 	     match EConstr.kind sigma type_of_hid with
 	       | Prod(_,_,t') ->
@@ -503,7 +502,7 @@ and intros_with_rewrite_aux : tactic =
   fun g ->
     let eq_ind = make_eq () in
     let sigma = project g in
-    match EConstr.kind sigma (EConstr.of_constr (pf_concl g)) with
+    match EConstr.kind sigma (pf_concl g) with
 	  | Prod(_,t,t') ->
 	      begin
 		match EConstr.kind sigma t with
@@ -591,7 +590,7 @@ and intros_with_rewrite_aux : tactic =
 let rec reflexivity_with_destruct_cases g =
   let destruct_case () =
     try
-      match EConstr.kind (project g) (snd (destApp (project g) (EConstr.of_constr (pf_concl g)))).(2) with
+      match EConstr.kind (project g) (snd (destApp (project g) (pf_concl g))).(2) with
 	| Case(_,_,v,_) ->
 	    tclTHENSEQ[
 	      Proofview.V82.of_tactic (simplest_case v);
@@ -608,7 +607,7 @@ let rec reflexivity_with_destruct_cases g =
 	 match sc with
 	     None -> tclIDTAC g
 	   | Some id ->
-	       match EConstr.kind (project g) (EConstr.of_constr (pf_unsafe_type_of g (mkVar id))) with
+	       match EConstr.kind (project g) (pf_unsafe_type_of g (mkVar id)) with
 		 | App(eq,[|_;t1;t2|]) when EConstr.eq_constr (project g) eq eq_ind ->
 		     if Equality.discriminable (pf_env g) (project g) t1 t2
 		     then Proofview.V82.of_tactic (Equality.discrHyp id) g
@@ -674,12 +673,11 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
     let f = funcs.(i) in
     let graph_principle = nf_zeta (EConstr.of_constr schemes.(i))  in
     let princ_type = pf_unsafe_type_of g graph_principle in
-    let princ_type = EConstr.of_constr princ_type in
     let princ_infos = Tactics.compute_elim_sig (project g) princ_type in
     (* Then we get the number of argument of the function
        and compute a fresh name for each of them
     *)
-    let nb_fun_args = nb_prod (project g) (EConstr.of_constr (pf_concl g)) - 2 in
+    let nb_fun_args = nb_prod (project g) (pf_concl g) - 2 in
     let args_names = generate_fresh_id (Id.of_string "x") [] nb_fun_args in
     let ids = args_names@(pf_ids_of_hyps g) in
     (* and fresh names for res H and the principle (cf bug bug #1174) *)
@@ -937,7 +935,6 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 let revert_graph kn post_tac hid g =
     let sigma = project g in
     let typ = pf_unsafe_type_of g (mkVar hid) in
-    let typ = EConstr.of_constr typ in
     match EConstr.kind sigma typ with
       | App(i,args) when isInd sigma i ->
 	  let ((kn',num) as ind'),u = destInd sigma i in
@@ -990,7 +987,6 @@ let functional_inversion kn hid fconst f_correct : tactic =
     let old_ids = List.fold_right Id.Set.add  (pf_ids_of_hyps g) Id.Set.empty in
     let sigma = project g in
     let type_of_h = pf_unsafe_type_of g (mkVar hid) in
-    let type_of_h = EConstr.of_constr type_of_h in
     match EConstr.kind sigma type_of_h with
       | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ())  ->
 	  let pre_tac,f_args,res =
@@ -1044,7 +1040,6 @@ let invfun qhyp f g =
 	  (fun hid -> Proofview.V82.tactic begin fun g ->
             let sigma = project g in
 	     let hyp_typ = pf_unsafe_type_of g (mkVar hid)  in
-	     let hyp_typ = EConstr.of_constr hyp_typ in
 	     match EConstr.kind sigma hyp_typ with
 	       | App(eq,args) when EConstr.eq_constr sigma eq (make_eq ()) ->
 		   begin
-- 
cgit v1.2.3


From c8c8ccdaaffefdbd3d78c844552a08bcb7b4f915 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 02:12:40 +0100
Subject: Evar-normalizing functions now act on EConstrs.

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

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 5cbec77437..dcec2cb74d 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -846,7 +846,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	   lem_id
 	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),((Decl_kinds.Proof Decl_kinds.Theorem)))
            !evd
-	   (EConstr.Unsafe.to_constr typ)
+	   typ
            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
 		   (Proofview.V82.tactic (observe_tac ("prove correctness ("^(Id.to_string f_id)^")")
@@ -908,7 +908,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	 let lem_id = mk_complete_id f_id in
 	 Lemmas.start_proof lem_id
 	   (Decl_kinds.Global,Flags.is_universe_polymorphism (),(Decl_kinds.Proof Decl_kinds.Theorem)) sigma
-	 (EConstr.Unsafe.to_constr (fst lemmas_types_infos.(i)))
+	 (fst lemmas_types_infos.(i))
            (Lemmas.mk_hook (fun _ _ -> ()));
 	 ignore (Pfedit.by
 	   (Proofview.V82.tactic (observe_tac ("prove completeness ("^(Id.to_string f_id)^")")
-- 
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/funind/invfun.ml | 20 +++++++-------------
 1 file changed, 7 insertions(+), 13 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index dcec2cb74d..8f1420940b 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -26,12 +26,6 @@ open Context.Rel.Declaration
 
 module RelDecl = Context.Rel.Declaration
 
-let local_assum (na, t) =
-  RelDecl.LocalAssum (na, EConstr.Unsafe.to_constr t)
-
-let local_def (na, b, t) =
-  RelDecl.LocalDef (na, EConstr.Unsafe.to_constr b, EConstr.Unsafe.to_constr t)
-
 (* Some pretty printing function for debugging purpose *)
 
 let pr_binding prc  =
@@ -147,7 +141,7 @@ let generate_type evd g_to_f f graph i =
   let fun_ctxt,res_type =
     match ctxt with
       | [] | [_] -> anomaly (Pp.str "Not a valid context")
-      | decl :: fun_ctxt -> fun_ctxt, EConstr.of_constr (RelDecl.get_type decl)
+      | decl :: fun_ctxt -> fun_ctxt, RelDecl.get_type decl
   in
   let rec args_from_decl i accu = function
   | [] -> accu
@@ -187,12 +181,12 @@ let generate_type evd g_to_f f graph i =
     \[\forall (x_1:t_1)\ldots(x_n:t_n), let fv := f x_1\ldots x_n in, forall res,  \]
     i*)
   let pre_ctxt =
-    local_assum (Name res_id, lift 1 res_type) :: local_def (Name fv_id, mkApp (f,args_as_rels), res_type) :: fun_ctxt
+    LocalAssum (Name res_id, lift 1 res_type) :: LocalDef (Name fv_id, mkApp (f,args_as_rels), res_type) :: fun_ctxt
   in
   (*i and we can return the solution depending on which lemma type we are defining i*)
   if g_to_f
-  then local_assum (Anonymous,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph
-  else local_assum (Anonymous,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph
+  then LocalAssum (Anonymous,graph_applied)::pre_ctxt,(lift 1 res_eq_f_of_args),graph
+  else LocalAssum (Anonymous,res_eq_f_of_args)::pre_ctxt,(lift 1 graph_applied),graph
 
 
 (*
@@ -280,7 +274,7 @@ let prove_fun_correct evd functional_induction funs_constr graphs_constr schemes
 	(fun decl ->
 	   List.map
 	     (fun id -> Loc.ghost, IntroNaming (IntroIdentifier id))
-	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (EConstr.of_constr (RelDecl.get_type decl))))))
+	     (generate_fresh_id (Id.of_string "y") ids (List.length (fst (decompose_prod_assum evd (RelDecl.get_type decl)))))
 	)
 	branches
     in
@@ -477,7 +471,7 @@ let generalize_dependent_of x hyp g =
   tclMAP
     (function
        | LocalAssum (id,t) when not (Id.equal id hyp) &&
-	   (Termops.occur_var (pf_env g) (project g) x (EConstr.of_constr t)) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
+	   (Termops.occur_var (pf_env g) (project g) x t) -> tclTHEN (Proofview.V82.of_tactic (Tactics.generalize [mkVar id])) (thin [id])
        | _ -> tclIDTAC
     )
     (pf_hyps g)
@@ -695,7 +689,7 @@ let prove_fun_complete funcs graphs schemes lemmas_types_infos i : tactic =
 	(fun decl ->
 	   List.map
 	     (fun id -> id)
-	     (generate_fresh_id (Id.of_string "y") ids (nb_prod (project g) (EConstr.of_constr (RelDecl.get_type decl))))
+	     (generate_fresh_id (Id.of_string "y") ids (nb_prod (project g) (RelDecl.get_type decl)))
 	)
 	branches
     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/funind/invfun.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

(limited to 'plugins/funind/invfun.ml')

diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 2c2cd919b1..94ec0a898a 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -783,7 +783,8 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
   assert (funs <> []);
   assert (graphs <> []);
   let funs = Array.of_list funs and graphs = Array.of_list graphs in
-  let funs_constr = Array.map mkConstU funs  in
+  let map (c, u) = mkConstU (c, EInstance.make u) in
+  let funs_constr = Array.map map funs  in
   States.with_state_protection_on_exception
     (fun () ->
      let env = Global.env () in
@@ -882,7 +883,7 @@ let derive_correctness make_scheme functional_induction (funs: pconstant list) (
 	(Indrec.build_mutual_induction_scheme (Global.env ()) !evd
 	   (Array.to_list
 	      (Array.mapi
-		 (fun i _ -> ((kn,i),u(* Univ.Instance.empty *)),true,InType)
+		 (fun i _ -> ((kn,i), EInstance.kind !evd u),true,InType)
 		 mib.Declarations.mind_packets
 	      )
 	   )
-- 
cgit v1.2.3