Evar maps contain econstrs.

We bootstrap the circular evar_map <-> econstr dependency by moving
the internal EConstr.API module to Evd.MiniEConstr. Then we make the
Evd functions use econstr.

5 files changed, 19 insertions, 25 deletions

diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index d04887a48..8da0e1c4f 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -1050,8 +1050,7 @@ let do_replace (evd:Evd.evar_map ref) params rec_arg_num rev_args_id f fun_num a
 	  (Global.env ()) !evd
 	  (Constrintern.locate_reference (qualid_of_ident equation_lemma_id))
       in
-      let res = EConstr.of_constr res in
-      evd:=evd';                       
+      evd:=evd';
       let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd res in 
       res
   in
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 804548ce5..04a23cdb9 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -266,7 +266,7 @@ let change_property_sort evd toSort princ princName =
       (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident princName)) in
   let init =
     let nargs =  (princ_info.nparams + (List.length  princ_info.predicates)) in
-    mkApp(princName_as_constr,
+    mkApp(EConstr.Unsafe.to_constr princName_as_constr,
 	  Array.init nargs
 	    (fun i -> mkRel (nargs - i )))
   in
@@ -630,11 +630,14 @@ let build_scheme fas =
 	    in
             let evd',f = Evd.fresh_global (Global.env ()) !evd f_as_constant in
             let _ = evd := evd' in 
-	    let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd (EConstr.of_constr f) in 
-            if isConst f
-            then (destConst f,sort)
-            else user_err Pp.(pr_constr_env (Global.env ()) !evd f ++spc () ++ str "should be the named of a globally defined function")
-	 )
+            let _ = Typing.e_type_of ~refresh:true (Global.env ()) evd f in
+            let c, u =
+              try EConstr.destConst !evd f
+              with DestKO ->
+                user_err Pp.(pr_econstr_env (Global.env ()) !evd f ++spc () ++ str "should be the named of a globally defined function")
+            in
+            (c, EConstr.EInstance.kind !evd u), sort
+         )
 	 fas
 		   ) in
   let bodies_types =
diff --git a/plugins/funind/glob_termops.ml b/plugins/funind/glob_termops.ml
index 40ea40b6b..845104c3c 100644
--- a/plugins/funind/glob_termops.ml
+++ b/plugins/funind/glob_termops.ml
@@ -564,6 +564,7 @@ let resolve_and_replace_implicits ?(flags=Pretyping.all_and_fail_flags) ?(expect
 If someone knows how to prevent solved existantial removal in  understand, please do not hesitate to change the computation of [ctx] here *) 
   let ctx,_,_ = Pretyping.ise_pretype_gen flags env sigma Glob_ops.empty_lvar expected_type rt in
   let ctx, f = Evarutil.nf_evars_and_universes ctx in
+  let f c = EConstr.of_constr (f (EConstr.Unsafe.to_constr c)) in
 
   (* then we map [rt] to replace the implicit holes by their values *)
   let rec change rt =
@@ -586,8 +587,8 @@ If someone knows how to prevent solved existantial removal in  understand, pleas
          with Found evi -> (* we found the evar corresponding to this hole *)
            match evi.evar_body with
            | Evar_defined c ->
-           (* we just have to lift the solution in glob_term *)
-              Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c))
+             (* we just have to lift the solution in glob_term *)
+              Detyping.detype Detyping.Now false Id.Set.empty env ctx (f c)
            | Evar_empty -> rt (* the hole was not solved : we do nothing *)
        )
     | (GHole(BinderType na,_,_)) -> (* we only want to deal with implicit arguments *)
@@ -609,7 +610,7 @@ If someone knows how to prevent solved existantial removal in  understand, pleas
                 match evi.evar_body with
                 | Evar_defined c ->
                    (* we just have to lift the solution in glob_term *)
-                   Detyping.detype Detyping.Now false Id.Set.empty env ctx (EConstr.of_constr (f c))
+                   Detyping.detype Detyping.Now false Id.Set.empty env ctx (f c)
                 | Evar_empty -> rt (* the hole was not solved : we d when falseo nothing *)
          in 
          res
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index d395e3601..748d8add2 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -77,8 +77,7 @@ let functional_induction with_clean c princl pat =
 		    user_err  (str "Cannot find induction principle for "
                                      ++ Printer.pr_leconstr_env (Tacmach.pf_env g) sigma (mkConst c') )
 	      in
-	      let princ = EConstr.of_constr princ in
-	      (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g')
+              (princ,NoBindings,Tacmach.pf_unsafe_type_of g' princ,g')
 	   | _ -> raise (UserError(None,str "functional induction must be used with a function" ))
 	 end
       | Some ((princ,binding)) ->
@@ -261,7 +260,6 @@ let derive_inversion fix_names =
 	 let evd,c =
 	   Evd.fresh_global
 	     (Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident id)) in 
-        let c = EConstr.of_constr c in
         let (cst, u) = destConst evd c in
 	 evd, (cst, EInstance.kind evd u) :: l
 	)
@@ -283,8 +281,7 @@ let derive_inversion fix_names =
 	       (Global.env ()) evd
 	       (Constrintern.locate_reference (Libnames.qualid_of_ident (mk_rel_id id)))
 	   in 
-	   let id = EConstr.of_constr id in
-	   evd,(fst (destInd evd id))::l
+           evd,(fst (destInd evd id))::l
 	  )
 	  fix_names
 	  (evd',[])
@@ -388,7 +385,7 @@ let generate_principle (evd:Evd.evar_map ref) pconstants on_error
 	     let evd = ref (Evd.from_env env) in
 	     let evd',uprinc = Evd.fresh_global env !evd princ in
              let _ = evd := evd' in 
-	     let princ_type = Typing.e_type_of ~refresh:true env evd (EConstr.of_constr uprinc) in
+             let princ_type = Typing.e_type_of ~refresh:true env evd uprinc in
 	     let princ_type = EConstr.Unsafe.to_constr princ_type in
     	     Functional_principles_types.generate_functional_principle
 	       evd
@@ -425,7 +422,6 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 	    let evd,c =
 	      Evd.fresh_global
 		(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
-            let c = EConstr.of_constr c in
             let (cst, u) = destConst evd c in
             let u = EInstance.kind evd u in
             evd,((cst, u) :: l)
@@ -442,7 +438,6 @@ let register_struct is_rec (fixpoint_exprl:(Vernacexpr.fixpoint_expr * Vernacexp
 	    let evd,c =
 	      Evd.fresh_global
 		(Global.env ()) evd (Constrintern.locate_reference (Libnames.qualid_of_ident fname)) in
-            let c = EConstr.of_constr c in
             let (cst, u) = destConst evd c in
             let u = EInstance.kind evd u in
             evd,((cst, u) :: l)
diff --git a/plugins/funind/invfun.ml b/plugins/funind/invfun.ml
index ae84eaa93..28e85268a 100644
--- a/plugins/funind/invfun.ml
+++ b/plugins/funind/invfun.ml
@@ -102,7 +102,6 @@ let generate_type evd g_to_f f graph i =
   let evd',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 graph in
   let ctxt,_ = decompose_prod_assum !evd graph_arity in
@@ -172,7 +171,6 @@ 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 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
@@ -823,8 +821,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive 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_constr = EConstr.of_constr lem_cst_constr in
-	 let (lem_cst,_) = destConst !evd lem_cst_constr in
+         let (lem_cst,_) = destConst !evd lem_cst_constr in
 	 update_Function {finfo with correctness_lemma = Some lem_cst};
 
       )
@@ -884,8 +881,7 @@ let derive_correctness make_scheme (funs: pconstant list) (graphs:inductive 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_constr = EConstr.of_constr lem_cst_constr in
-	 let (lem_cst,_) = destConst !evd lem_cst_constr in
+         let (lem_cst,_) = destConst !evd lem_cst_constr in
 	 update_Function {finfo with completeness_lemma = Some lem_cst}
       )
       funs)