Equality API using EConstr.

6 files changed, 25 insertions, 23 deletions

diff --git a/plugins/cc/cctac.ml b/plugins/cc/cctac.ml
index 7b023413d..a12ef00ec 100644
--- a/plugins/cc/cctac.ml
+++ b/plugins/cc/cctac.ml
@@ -229,7 +229,8 @@ let make_prb gls depth additionnal_terms =
 
 let build_projection intype (cstr:pconstructor) special default gls=
   let ci= (snd(fst cstr)) in
-  let body=Equality.build_selector (pf_env gls) (project gls) ci (mkRel 1) intype special default in
+  let body=Equality.build_selector (pf_env gls) (project gls) ci (EConstr.mkRel 1) (EConstr.of_constr intype) (EConstr.of_constr special) (EConstr.of_constr default) in
+  let body = EConstr.Unsafe.to_constr body in
   let id=pf_get_new_id (Id.of_string "t") gls in
     mkLambda(Name id,intype,body)
 
diff --git a/plugins/fourier/fourierR.ml b/plugins/fourier/fourierR.ml
index fa64b276c..dbb5cc2de 100644
--- a/plugins/fourier/fourierR.ml
+++ b/plugins/fourier/fourierR.ml
@@ -600,15 +600,15 @@ let rec fourier () =
 		      (Tacticals.New.tclTHEN (apply (if sres then get coq_Rnot_lt_lt
 					       else get coq_Rnot_le_le))
 			    (Tacticals.New.tclTHENS (Equality.replace
-				       (mkAppL [|cget coq_Rminus;!t2;!t1|]
-					       )
-				       tc)
+				       (EConstr.of_constr (mkAppL [|cget coq_Rminus;!t2;!t1|]
+					       ))
+				       (EConstr.of_constr tc))
 		 	       [tac2;
                                 (Tacticals.New.tclTHENS
 				  (Equality.replace
-				    (mkApp (cget coq_Rinv,
-				      [|cget coq_R1|]))
-				    (cget coq_R1))
+				    (EConstr.of_constr (mkApp (cget coq_Rinv,
+				      [|cget coq_R1|])))
+				    (get coq_R1))
 (* en attendant Field, ça peut aider Ring de remplacer 1/1 par 1 ... *)
 
       			        [Tacticals.New.tclORELSE
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 940f1669a..2e3992be9 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -401,7 +401,7 @@ let rewrite_until_var arg_num eq_ids : tactic =
 	| [] -> anomaly (Pp.str "Cannot find a way to prove recursive property");
 	| eq_id::eq_ids ->
 	    tclTHEN
-	      (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (mkVar eq_id))))
+	      (tclTRY (Proofview.V82.of_tactic (Equality.rewriteRL (EConstr.mkVar eq_id))))
 	      (do_rewrite eq_ids)
 	      g
   in
@@ -1060,7 +1060,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
 	  let just_introduced = nLastDecls nb_intro_to_do g' in
           let open Context.Named.Declaration in
 	  let just_introduced_id = List.map get_id just_introduced in
-	  tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR equation_lemma))
+	  tclTHEN (Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.of_constr equation_lemma)))
 		  (revert just_introduced_id) g'
       )
       g
@@ -1425,7 +1425,7 @@ let prove_with_tcc tcc_lemma_constr eqs : tactic =
 
 let backtrack_eqs_until_hrec hrec eqs : tactic =
   fun gls ->
-    let eqs = List.map mkVar eqs in
+    let eqs = List.map EConstr.mkVar eqs in
     let rewrite =
       tclFIRST (List.map (fun x -> Proofview.V82.of_tactic (Equality.rewriteRL x)) eqs )
     in
@@ -1453,7 +1453,7 @@ let rec rewrite_eqs_in_eqs eqs =
 		  observe_tac
 		    (Format.sprintf "rewrite %s in %s " (Id.to_string eq) (Id.to_string id))
 		    (tclTRY (Proofview.V82.of_tactic (Equality.general_rewrite_in true Locus.AllOccurrences
-			       true (* dep proofs also: *) true id (mkVar eq) false)))
+			       true (* dep proofs also: *) true id (EConstr.mkVar eq) false)))
 		    gl
 	       )
 	       eqs
@@ -1659,7 +1659,7 @@ let prove_principle_for_gen
       (* observe_tac "h_fix " *) (Proofview.V82.of_tactic (fix (Some fix_id) (List.length args_ids + 1)));
 (*       (fun g -> observe (Printer.pr_goal (sig_it g) ++ fnl() ++ pr_lconstr_env (pf_env g ) (pf_unsafe_type_of g (mkVar fix_id) )); tclIDTAC g); *)
       h_intros (List.rev (acc_rec_arg_id::args_ids));
-      Proofview.V82.of_tactic (Equality.rewriteLR (mkConst eq_ref));
+      Proofview.V82.of_tactic (Equality.rewriteLR (EConstr.of_constr (mkConst eq_ref)));
       (* observe_tac "finish" *) (fun gl' ->
 	 let body =
 	   let _,args = destApp (pf_concl gl') in
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index a45effb16..08b40a1f7 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -502,6 +502,7 @@ let evaluable_of_global_reference r = (* Tacred.evaluable_of_global_reference (G
     | _ -> assert false;;
 
 let list_rewrite (rev:bool) (eqs: (constr*bool) list) =
+  let eqs = List.map (Util.on_fst EConstr.of_constr) eqs in
   tclREPEAT
     (List.fold_right
        (fun (eq,b) i -> tclORELSE (Proofview.V82.of_tactic ((if b then Equality.rewriteLR else Equality.rewriteRL) eq)) i)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index 36fb6dad3..d29d4694f 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
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 74affa396..5cee3cb20 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -871,10 +871,10 @@ let rec make_rewrite_list expr_info max = function
 	  in
 	  Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
-	    (mkVar hp,
+	    (EConstr.mkVar hp,
 	     ExplicitBindings[Loc.ghost,NamedHyp def,
-			      expr_info.f_constr;Loc.ghost,NamedHyp k,
-			      (f_S max)]) false) g) )
+			      EConstr.of_constr expr_info.f_constr;Loc.ghost,NamedHyp k,
+			      EConstr.of_constr (f_S max)]) false) g) )
       )
       [make_rewrite_list expr_info max l;
        observe_tclTHENLIST (str "make_rewrite_list")[ (* x < S max proof *)
@@ -898,10 +898,10 @@ let make_rewrite expr_info l hp max =
 	 observe_tac (str "general_rewrite_bindings")
 	   (Proofview.V82.of_tactic (general_rewrite_bindings false Locus.AllOccurrences
 	    true (* dep proofs also: *) true 
-	    (mkVar hp,
+	    (EConstr.mkVar hp,
 	     ExplicitBindings[Loc.ghost,NamedHyp def,
-			      expr_info.f_constr;Loc.ghost,NamedHyp k,
-			      (f_S (f_S max))]) false)) g)
+			      EConstr.of_constr expr_info.f_constr;Loc.ghost,NamedHyp k,
+			      EConstr.of_constr (f_S (f_S max))]) false)) g)
        [observe_tac(str "make_rewrite finalize") (
 	 (* tclORELSE( h_reflexivity) *)
 	 (observe_tclTHENLIST (str "make_rewrite")[