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.

6 files changed, 27 insertions, 33 deletions

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 03ff580ad..aeaf16723 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -62,9 +62,6 @@ let clenv_get_type_of ce c = Retyping.get_type_of (cl_env ce) (cl_sigma ce) c
 
 exception NotExtensibleClause
 
-let mk_freelisted c =
-  map_fl EConstr.of_constr (mk_freelisted (EConstr.Unsafe.to_constr c))
-
 let clenv_push_prod cl =
   let typ = whd_all (cl_env cl) (cl_sigma cl) (clenv_type cl) in
   let rec clrec typ = match EConstr.kind cl.evd typ with
@@ -73,7 +70,7 @@ let clenv_push_prod cl =
 	let mv = new_meta () in
 	let dep = not (noccurn (cl_sigma cl) 1 u) in
 	let na' = if dep then na else Anonymous in
-	let e' = meta_declare mv (EConstr.Unsafe.to_constr t) ~name:na' cl.evd in
+        let e' = meta_declare mv t ~name:na' cl.evd in
 	let concl = if dep then subst1 (mkMeta mv) u else u in
 	let def = applist (cl.templval.rebus,[mkMeta mv]) in
 	{ templval = mk_freelisted def;
@@ -107,8 +104,7 @@ let clenv_environments evd bound t =
 	  let mv = new_meta () in
 	  let dep = not (noccurn evd 1 t2) in
 	  let na' = if dep then na else Anonymous in
-	  let t1 = EConstr.Unsafe.to_constr t1 in
-	  let e' = meta_declare mv t1 ~name:na' e in
+          let e' = meta_declare mv t1 ~name:na' e in
 	  clrec (e', (mkMeta mv)::metas) (Option.map ((+) (-1)) n)
 	    (if dep then (subst1 (mkMeta mv) t2) else t2)
       | (n, LetIn (na,b,_,t)) -> clrec (e,metas) n (subst1 b t)
@@ -167,13 +163,13 @@ let clenv_assign mv rhs clenv =
     user_err Pp.(str "clenv_assign: circularity in unification");
   try
     if meta_defined clenv.evd mv then
-      if not (EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd mv)).rebus) rhs) then
+      if not (EConstr.eq_constr clenv.evd (fst (meta_fvalue clenv.evd mv)).rebus rhs) then
         error_incompatible_inst clenv mv
       else
 	clenv
     else
       let st = (Conv,TypeNotProcessed) in
-      {clenv with evd = meta_assign mv (EConstr.Unsafe.to_constr rhs_fls.rebus,st) clenv.evd}
+      {clenv with evd = meta_assign mv (rhs_fls.rebus,st) clenv.evd}
   with Not_found ->
     user_err Pp.(str "clenv_assign: undefined meta")
 
@@ -218,7 +214,7 @@ let clenv_assign mv rhs clenv =
 *)
 
 let clenv_metas_in_type_of_meta evd mv =
-  (mk_freelisted (meta_instance evd (map_fl EConstr.of_constr (meta_ftype evd mv)))).freemetas
+  (mk_freelisted (meta_instance evd (meta_ftype evd mv))).freemetas
 
 let dependent_in_type_of_metas clenv mvs =
   List.fold_right
@@ -288,11 +284,11 @@ let adjust_meta_source evd mv = function
        in situations like "ex_intro (fun x => P) ?ev p" *)
     let f = function (mv',(Cltyp (_,t) | Clval (_,_,t))) ->
       if Metaset.mem mv t.freemetas then
-        let f,l = decompose_app evd (EConstr.of_constr t.rebus) in
+        let f,l = decompose_app evd t.rebus in
         match EConstr.kind evd f with
         | Meta mv'' ->
           (match meta_opt_fvalue evd mv'' with
-          | Some (c,_) -> match_name (EConstr.of_constr c.rebus) l
+          | Some (c,_) -> match_name c.rebus l
           | None -> None)
         | _ -> None
       else None in
@@ -502,7 +498,6 @@ let clenv_assign_binding clenv k c =
   let k_typ = clenv_hnf_constr clenv (clenv_meta_type clenv k) in
   let c_typ = nf_betaiota clenv.env clenv.evd (clenv_get_type_of clenv c) in
   let status,clenv',c = clenv_unify_binding_type clenv c c_typ k_typ in
-  let c = EConstr.Unsafe.to_constr c in
   { clenv' with evd = meta_assign k (c,(Conv,status)) clenv'.evd }
 
 let clenv_match_args bl clenv =
@@ -515,7 +510,7 @@ let clenv_match_args bl clenv =
       (fun clenv {CAst.loc;v=(b,c)} ->
 	let k = meta_of_binder clenv loc mvs b in
         if meta_defined clenv.evd k then
-          if EConstr.eq_constr clenv.evd (EConstr.of_constr (fst (meta_fvalue clenv.evd k)).rebus) c then clenv
+          if EConstr.eq_constr clenv.evd (fst (meta_fvalue clenv.evd k)).rebus c then clenv
           else error_already_defined b
         else
 	  clenv_assign_binding clenv k c)
@@ -677,7 +672,7 @@ let define_with_type sigma env ev c =
   let j = Environ.make_judge c ty in
   let (sigma, j) = Coercion.inh_conv_coerce_to true env sigma j t in
   let (ev, _) = destEvar sigma ev in
-  let sigma = Evd.define ev (EConstr.Unsafe.to_constr j.Environ.uj_val) sigma in
+  let sigma = Evd.define ev j.Environ.uj_val sigma in
   sigma
 
 let solve_evar_clause env sigma hyp_only clause = function
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 0d197c92c..c80f370fd 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -25,8 +25,6 @@ open Ltac_pretype
 type glob_constr_ltac_closure = ltac_var_map * glob_constr
 
 let depends_on_evar sigma evk _ (pbty,_,t1,t2) =
-  let t1 = EConstr.of_constr t1 in
-  let t2 = EConstr.of_constr t2 in
   try Evar.equal (head_evar sigma t1) evk
   with NoHeadEvar ->
   try Evar.equal (head_evar sigma t2) evk
@@ -35,12 +33,12 @@ let depends_on_evar sigma evk _ (pbty,_,t1,t2) =
 let define_and_solve_constraints evk c env evd =
   if Termops.occur_evar evd evk c then
     Pretype_errors.error_occur_check env evd evk c;
-  let evd = define evk (EConstr.Unsafe.to_constr c) evd in
+  let evd = define evk c evd in
   let (evd,pbs) = extract_changed_conv_pbs evd (depends_on_evar evd evk) in
   match
     List.fold_left
       (fun p (pbty,env,t1,t2) -> match p with
-	| Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty (EConstr.of_constr t1) (EConstr.of_constr t2)
+        | Success evd -> Evarconv.evar_conv_x full_transparent_state env evd pbty t1 t2
 	| UnifFailure _ as x -> x) (Success evd)
       pbs
   with
@@ -59,7 +57,7 @@ let w_refine (evk,evi) (ltac_var,rawc) sigma =
       Pretyping.fail_evar = false;
       Pretyping.expand_evars = true } in
     try Pretyping.understand_ltac flags
-      env sigma ltac_var (Pretyping.OfType (EConstr.of_constr evi.evar_concl)) rawc
+      env sigma ltac_var (Pretyping.OfType evi.evar_concl) rawc
     with e when CErrors.noncritical e ->
       let loc = Glob_ops.loc_of_glob_constr rawc in
       user_err ?loc 
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 6912db364..1440d1636 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -48,7 +48,7 @@ module V82 = struct
   (* Access to ".evar_concl" *)
   let concl evars gl =
     let evi = Evd.find evars gl in
-    EConstr.of_constr evi.Evd.evar_concl
+    evi.Evd.evar_concl
 
   (* Access to ".evar_extra" *)
   let extra evars gl =
@@ -61,7 +61,6 @@ module V82 = struct
        be shelved. It must not appear as a future_goal, so the future
        goals are restored to their initial value after the evar is
        created. *)
-    let concl = EConstr.Unsafe.to_constr concl in
     let prev_future_goals = Evd.save_future_goals evars in
     let evi = { Evd.evar_hyps = hyps;
 		Evd.evar_concl = concl;
@@ -86,7 +85,7 @@ module V82 = struct
       if not (Evarutil.occur_evar_upto sigma evk c) then ()
       else Pretype_errors.error_occur_check Environ.empty_env sigma evk c
     in
-    Evd.define evk (EConstr.Unsafe.to_constr c) sigma
+    Evd.define evk c sigma
 
   (* Instantiates a goal with an open term, using name of goal for evk' *)
   let partial_solution_to sigma evk evk' c =
@@ -100,7 +99,9 @@ module V82 = struct
   let same_goal evars1 gl1 evars2 gl2 =
     let evi1 = Evd.find evars1 gl1 in
     let evi2 = Evd.find evars2 gl2 in
-    Constr.equal evi1.Evd.evar_concl evi2.Evd.evar_concl &&
+    let c1 = EConstr.Unsafe.to_constr evi1.Evd.evar_concl in
+    let c2 = EConstr.Unsafe.to_constr evi2.Evd.evar_concl in
+    Constr.equal c1 c2 &&
     Environ.eq_named_context_val evi1.Evd.evar_hyps evi2.Evd.evar_hyps
 
   let weak_progress glss gls =
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 8725f51cd..abda04ff1 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -233,7 +233,7 @@ let apply_implicit_tactic tac = (); fun env sigma evk ->
 	(Environ.named_context env) ->
       let tac = Proofview.tclTHEN tac (Proofview.tclEXTEND [] (Proofview.tclZERO (CErrors.UserError (None,Pp.str"Proof is not complete."))) []) in
       (try
-        let c = Evarutil.nf_evars_universes sigma evi.evar_concl in
+        let c = Evarutil.nf_evars_universes sigma (EConstr.Unsafe.to_constr evi.evar_concl) in
         let c = EConstr.of_constr c in
         if Evarutil.has_undefined_evars sigma c then raise Exit;
         let (ans, _, ctx) =
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index d6c0e3341..fc7c437e6 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -340,7 +340,7 @@ let close_proof ~keep_body_ucst_separate ?feedback_id ~now
      have existential variables in the initial types of goals, we need to
      normalise them for the kernel. *)
   let subst_evar k =
-    Proof.in_proof proof (fun m -> Evd.existential_opt_value m k) in
+    Proof.in_proof proof (fun m -> Evd.existential_opt_value0 m k) in
   let nf = Universes.nf_evars_and_universes_opt_subst subst_evar
     (UState.subst universes) in
   let make_body =
diff --git a/proofs/refine.ml b/proofs/refine.ml
index 909556b1e..5a2d82977 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -15,7 +15,7 @@ open Context.Named.Declaration
 module NamedDecl = Context.Named.Declaration
 
 let extract_prefix env info =
-  let ctx1 = List.rev (Environ.named_context env) in
+  let ctx1 = List.rev (EConstr.named_context env) in
   let ctx2 = List.rev (Evd.evar_context info) in
   let rec share l1 l2 accu = match l1, l2 with
   | d1 :: l1, d2 :: l2 ->
@@ -29,21 +29,21 @@ let typecheck_evar ev env sigma =
   let info = Evd.find sigma ev in
   (** Typecheck the hypotheses. *)
   let type_hyp (sigma, env) decl =
-    let t = EConstr.of_constr (NamedDecl.get_type decl) in
+    let t = NamedDecl.get_type decl in
     let evdref = ref sigma in
     let _ = Typing.e_sort_of env evdref t in
     let () = match decl with
     | LocalAssum _ -> ()
-    | LocalDef (_,body,_) -> Typing.e_check env evdref (EConstr.of_constr body) t
+    | LocalDef (_,body,_) -> Typing.e_check env evdref body t
     in
-    (!evdref, Environ.push_named decl env)
+    (!evdref, EConstr.push_named decl env)
   in
   let (common, changed) = extract_prefix env info in
-  let env = Environ.reset_with_named_context (Environ.val_of_named_context common) env in
+  let env = Environ.reset_with_named_context (EConstr.val_of_named_context common) env in
   let (sigma, env) = List.fold_left type_hyp (sigma, env) changed in
   (** Typecheck the conclusion *)
   let evdref = ref sigma in
-  let _ = Typing.e_sort_of env evdref (EConstr.of_constr (Evd.evar_concl info)) in
+  let _ = Typing.e_sort_of env evdref (Evd.evar_concl info) in
   !evdref
 
 let typecheck_proof c concl env sigma =
@@ -106,7 +106,6 @@ let generic_refine ~typecheck f gl =
   let evs = Evd.map_filter_future_goals (Proofview.Unsafe.advance sigma) evs in
   let comb,shelf,given_up,evkmain = Evd.dispatch_future_goals evs in
   (** Proceed to the refinement *)
-  let c = EConstr.Unsafe.to_constr c in
   let sigma = match Proofview.Unsafe.advance sigma self with
   | None ->
     (** Nothing to do, the goal has been solved by side-effect *)
@@ -124,7 +123,8 @@ let generic_refine ~typecheck f gl =
   (** Mark goals *)
   let sigma = CList.fold_left Proofview.Unsafe.mark_as_goal sigma comb in
   let comb = CList.map (fun x -> Proofview.goal_with_state x state) comb in
-  let trace () = Pp.(hov 2 (str"simple refine"++spc()++ Hook.get pr_constrv env sigma c)) in
+  let trace () = Pp.(hov 2 (str"simple refine"++spc()++
+                            Hook.get pr_constrv env sigma (EConstr.Unsafe.to_constr c))) in
   Proofview.Trace.name_tactic trace (Proofview.tclUNIT v) >>= fun v ->
   Proofview.Unsafe.tclSETENV (Environ.reset_context env) <*>
   Proofview.Unsafe.tclEVARS sigma <*>