Reductionops API using EConstr.

6 files changed, 27 insertions, 27 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index f6567ab812..258ee5ad69 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -318,7 +318,7 @@ let change_eq env sigma hyp_id (context:Context.Rel.t) x t end_of_type  =
 	context
     in
     let new_type_of_hyp =
-      Reductionops.nf_betaiota Evd.empty new_type_of_hyp in
+      Reductionops.nf_betaiota Evd.empty (EConstr.of_constr new_type_of_hyp) in
     let new_ctxt,new_end_of_type =
       decompose_prod_n_assum ctxt_size new_type_of_hyp
     in
@@ -786,7 +786,7 @@ let build_proof
 		      do_finalize dyn_infos  g
 		  | Lambda _ ->
 		      let new_term =
-                        Reductionops.nf_beta Evd.empty dyn_infos.info in
+                        Reductionops.nf_beta Evd.empty (EConstr.of_constr dyn_infos.info) in
 		      build_proof do_finalize {dyn_infos with info = new_term}
 			g
 		  | LetIn _ ->
@@ -1090,7 +1090,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	       (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
 	       (Global.env ())
 	       (Evd.empty)
-	       body
+	       (EConstr.of_constr body)
 	| None -> error ( "Cannot define a principle over an axiom ")
     in
     let fbody = get_body fnames.(fun_num) in
@@ -1142,8 +1142,8 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 	      Array.map
 		(fun body ->
 		   Reductionops.nf_betaiota Evd.empty
-		     (applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body,
-			      List.rev_map var_of_decl princ_params))
+		     (EConstr.of_constr (applist(substl (List.rev (Array.to_list all_funs_with_full_params)) body,
+			      List.rev_map var_of_decl princ_params)))
 		)
 		bodies
 	    in
@@ -1179,20 +1179,20 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		   let body_with_param,num =
 		     let body = get_body fnames.(i) in
 		     let body_with_full_params =
-		       Reductionops.nf_betaiota Evd.empty (
-			 applist(body,List.rev_map var_of_decl full_params))
+		       Reductionops.nf_betaiota Evd.empty (EConstr.of_constr (
+			 applist(body,List.rev_map var_of_decl full_params)))
 		     in
 		     match kind_of_term body_with_full_params with
 		       | Fix((_,num),(_,_,bs)) ->
 			       Reductionops.nf_betaiota Evd.empty
-				 (
+				 (EConstr.of_constr (
 				   (applist
 				      (substl
 					 (List.rev
 					    (Array.to_list all_funs_with_full_params))
 					 bs.(num),
 				       List.rev_map var_of_decl princ_params))
-				 ),num
+				 )),num
 			 | _ -> error "Not a mutual block"
 		   in
 		   let info =
@@ -1269,7 +1269,7 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		     rec_hyps = [];
 		     info =
 		       Reductionops.nf_betaiota Evd.empty
-			 (applist(fix_body,List.rev_map mkVar args_id));
+			 (EConstr.of_constr (applist(fix_body,List.rev_map mkVar args_id)));
 		     eq_hyps = []
 		   }
 		 in
@@ -1329,10 +1329,10 @@ let prove_princ_for_struct (evd:Evd.evar_map ref) interactive_proof fun_num fnam
 		     rec_hyps = [];
 		     info =
 		       Reductionops.nf_betaiota Evd.empty
-			 (applist(fbody_with_full_params,
+			 (EConstr.of_constr (applist(fbody_with_full_params,
 				  (List.rev_map var_of_decl princ_params)@
 				    (List.rev_map mkVar args_id)
-				 ));
+				 )));
 		     eq_hyps = []
 		   }
 		 in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 032d887de7..9637632a6c 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -405,7 +405,7 @@ let get_funs_constant mp dp =
 	      (CClosure.RedFlags.mkflags [CClosure.RedFlags.fZETA])
 	      (Global.env ())
 	      (Evd.from_env (Global.env ()))
-	      body
+	      (EConstr.of_constr body)
 	    in
 	    body
 	| None -> error ( "Cannot define a principle over an axiom ")
diff --git a/plugins/funind/glob_term_to_relation.ml b/plugins/funind/glob_term_to_relation.ml
index de2e5ea4e2..92de4d8734 100644
--- a/plugins/funind/glob_term_to_relation.ml
+++ b/plugins/funind/glob_term_to_relation.ml
@@ -352,7 +352,7 @@ let add_pat_variables pat typ env : Environ.env =
       | PatVar(_,na) -> Environ.push_rel (RelDecl.LocalAssum (na,typ)) env
       | PatCstr(_,c,patl,na) ->
 	  let Inductiveops.IndType(indf,indargs) =
-	    try Inductiveops.find_rectype env (Evd.from_env env) typ
+	    try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ)
 	    with Not_found -> assert false
 	  in
 	  let constructors = Inductiveops.get_constructors env indf in
@@ -409,7 +409,7 @@ let rec pattern_to_term_and_type env typ  = function
 	  constr
       in
       let Inductiveops.IndType(indf,indargs) =
-	try Inductiveops.find_rectype env (Evd.from_env env) typ
+	try Inductiveops.find_rectype env (Evd.from_env env) (EConstr.of_constr typ)
 	with Not_found -> assert false
       in
       let constructors = Inductiveops.get_constructors env indf in
@@ -629,7 +629,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
 	let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
 	let (ind,_) =
-	  try Inductiveops.find_inductive env (Evd.from_env env) b_typ
+	  try Inductiveops.find_inductive env (Evd.from_env env) (EConstr.of_constr b_typ)
 	  with Not_found ->
 	    user_err  (str "Cannot find the inductive associated to " ++
 			       Printer.pr_glob_constr b ++ str " in " ++
@@ -661,7 +661,7 @@ let rec build_entry_lc env funnames avoid rt  : glob_constr build_entry_return =
 	  let b_as_constr,ctx = Pretyping.understand env (Evd.from_env env) b in
 	  let b_typ = Typing.unsafe_type_of env (Evd.from_env env) b_as_constr in
 	  let (ind,_) =
-	    try Inductiveops.find_inductive env (Evd.from_env env) b_typ
+	    try Inductiveops.find_inductive env (Evd.from_env env) (EConstr.of_constr b_typ)
 	    with Not_found ->
 	      user_err  (str "Cannot find the inductive associated to " ++
 				 Printer.pr_glob_constr b ++ str " in " ++
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
 	)
diff --git a/plugins/funind/merge.ml b/plugins/funind/merge.ml
index 865042afbe..222c0c8043 100644
--- a/plugins/funind/merge.ml
+++ b/plugins/funind/merge.ml
@@ -135,7 +135,7 @@ let prNamedRLDecl s lc =
 
 let showind (id:Id.t) =
   let cstrid = Constrintern.global_reference id in
-  let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty cstrid in
+  let ind1,cstrlist = Inductiveops.find_inductive (Global.env()) Evd.empty (EConstr.of_constr cstrid) in
   let mib1,ib1 = Inductive.lookup_mind_specif (Global.env()) (fst ind1) in
   List.iter (fun decl ->
     print_string (string_of_name (Context.Rel.Declaration.get_name decl) ^ ":");
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index 6b63d7771e..4fd9e0ff89 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -693,7 +693,7 @@ let mkDestructEq :
       (fun g2 ->
         let changefun patvars = { run = fun sigma ->
           let redfun = pattern_occs [Locus.AllOccurrencesBut [1], expr] in
-          redfun.Reductionops.e_redfun (pf_env g2) sigma (pf_concl g2)
+          redfun.Reductionops.e_redfun (pf_env g2) sigma (EConstr.of_constr (pf_concl g2))
         } in
 	Proofview.V82.of_tactic (change_in_concl None changefun) g2);
       Proofview.V82.of_tactic (simplest_case expr)]), to_revert
@@ -1499,7 +1499,7 @@ let recursive_definition is_mes function_name rec_impls type_of_f r rec_arg_num
  (* Pp.msgnl (str "lemma type := " ++ Printer.pr_lconstr equation_lemma_type ++ fnl ()); *)
   let res_vars,eq' = decompose_prod equation_lemma_type in
   let env_eq' = Environ.push_rel_context (List.map (fun (x,y) -> LocalAssum (x,y)) res_vars) env in
-  let eq' = nf_zeta env_eq' eq'  in
+  let eq' = nf_zeta env_eq' (EConstr.of_constr eq') in
   let res =
 (*     Pp.msgnl (str "res_var :=" ++ Printer.pr_lconstr_env (push_rel_context (List.map (function (x,t) -> (x,None,t)) res_vars) env) eq'); *)
 (*     Pp.msgnl (str "rec_arg_num := " ++ str (string_of_int rec_arg_num)); *)