Goal API using EConstr.

13 files changed, 40 insertions, 29 deletions

diff --git a/ide/ide_slave.ml b/ide/ide_slave.ml
index 48fd0a93e4..c11c785877 100644
--- a/ide/ide_slave.ml
+++ b/ide/ide_slave.ml
@@ -191,7 +191,7 @@ let process_goal sigma g =
   let min_env = Environ.reset_context env in
   let id = Goal.uid g in
   let ccl =
-    let norm_constr = Reductionops.nf_evar sigma (Goal.V82.concl sigma g) in
+    let norm_constr = Reductionops.nf_evar sigma (EConstr.Unsafe.to_constr (Goal.V82.concl sigma g)) in
     Richpp.richpp_of_pp (pr_goal_concl_style_env env sigma norm_constr)
   in
   let process_hyp d (env,l) =
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index 44cd22c8bb..3bb6f1b5d5 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -41,7 +41,7 @@ let clear ids { it = goal; sigma } =
   let ids = List.fold_left (fun accu x -> Id.Set.add x accu) Id.Set.empty ids in
   let env = Goal.V82.env sigma goal in
   let sign = Goal.V82.hyps sigma goal in
-  let cl = Goal.V82.concl sigma goal in
+  let cl = EConstr.Unsafe.to_constr (Goal.V82.concl sigma goal) in
   let evdref = ref (Evd.clear_metas sigma) in
   let (hyps, concl) =
     try Evarutil.clear_hyps_in_evi env evdref sign cl ids
@@ -49,7 +49,7 @@ let clear ids { it = goal; sigma } =
       user_err  (str "Cannot clear " ++ pr_id id)
   in
   let sigma = !evdref in
-  let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
+  let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps (EConstr.of_constr concl) (Goal.V82.extra sigma goal) in
   let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
   { it = [gl]; sigma }
 
@@ -74,7 +74,7 @@ let tcl_change_info_gen info_gen =
      let concl = pf_concl gls in
      let hyps = Goal.V82.hyps (project gls) it in
      let extra = Goal.V82.extra (project gls) it in
-     let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps concl (info_gen extra) in
+     let (gl,ev,sigma) = Goal.V82.mk_goal (project gls) hyps (EConstr.of_constr concl) (info_gen extra) in
      let sigma = Goal.V82.partial_solution sigma it ev in
      { it = [gl] ; sigma= sigma; } )
 
diff --git a/plugins/decl_mode/g_decl_mode.ml4 b/plugins/decl_mode/g_decl_mode.ml4
index 18a35c6cfb..9e2c9f5973 100644
--- a/plugins/decl_mode/g_decl_mode.ml4
+++ b/plugins/decl_mode/g_decl_mode.ml4
@@ -25,7 +25,7 @@ open Ppdecl_proof
 let pr_goal gs =
   let (g,sigma) = Goal.V82.nf_evar (Tacmach.project gs) (Evd.sig_it gs) in
   let env = Goal.V82.env sigma g in
-  let concl = Goal.V82.concl sigma g in
+  let concl = EConstr.Unsafe.to_constr (Goal.V82.concl sigma g) in
   let goal =
     Printer.pr_context_of env sigma ++ cut () ++
       str "============================" ++ cut ()  ++
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index b0a3e839b9..089e76d7a0 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -172,7 +172,7 @@ let ltac_apply (f : Value.t) (args: Tacinterp.Value.t list) =
 
 let dummy_goal env sigma =
   let (gl,_,sigma) = 
-    Goal.V82.mk_goal sigma (named_context_val env) mkProp Evd.Store.empty in
+    Goal.V82.mk_goal sigma (named_context_val env) EConstr.mkProp Evd.Store.empty in
   {Evd.it = gl; Evd.sigma = sigma}
 
 let constr_of v = match Value.to_constr v with
diff --git a/plugins/ssrmatching/ssrmatching.ml4 b/plugins/ssrmatching/ssrmatching.ml4
index 308fb414ee..7f628f1650 100644
--- a/plugins/ssrmatching/ssrmatching.ml4
+++ b/plugins/ssrmatching/ssrmatching.ml4
@@ -1078,7 +1078,7 @@ END
 let thin id sigma goal =
   let ids = Id.Set.singleton id in
   let env = Goal.V82.env sigma goal in
-  let cl = Goal.V82.concl sigma goal in
+  let cl = EConstr.Unsafe.to_constr (Goal.V82.concl sigma goal) in
   let evdref = ref (Evd.clear_metas sigma) in
   let ans =
     try Some (Evarutil.clear_hyps_in_evi env evdref (Environ.named_context_val env) cl ids)
@@ -1088,7 +1088,7 @@ let thin id sigma goal =
   | None -> sigma
   | Some (hyps, concl) ->
     let sigma = !evdref in
-    let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) in
+    let (gl,ev,sigma) = Goal.V82.mk_goal sigma hyps (EConstr.of_constr concl) (Goal.V82.extra sigma goal) in
     let sigma = Goal.V82.partial_solution_to sigma goal gl ev in
     sigma
 
diff --git a/printing/printer.ml b/printing/printer.ml
index b36df27ed3..ed6ebdc9b6 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -384,7 +384,7 @@ let pr_transparent_state (ids, csts) =
 let default_pr_goal gs =
   let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in
   let env = Goal.V82.env sigma g in
-  let concl = Goal.V82.concl sigma g in
+  let concl = EConstr.Unsafe.to_constr (Goal.V82.concl sigma g) in
   let goal =
     pr_context_of env sigma ++ cut () ++
       str "============================" ++ cut ()  ++
@@ -407,7 +407,7 @@ let pr_goal_name sigma g =
 let pr_concl n sigma g =
   let (g,sigma) = Goal.V82.nf_evar sigma g in
   let env = Goal.V82.env sigma g in
-  let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in
+  let pc = pr_goal_concl_style_env env sigma (EConstr.Unsafe.to_constr (Goal.V82.concl sigma g)) in
     str (emacs_str "")  ++
       str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g ++
       str " is:" ++ cut () ++ str" "  ++ pc
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 956be88c8a..67ed5daaa1 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -264,6 +264,7 @@ let clenv_unify_meta_types ?(flags=default_unify_flags ()) clenv =
 
 let clenv_unique_resolver ?(flags=default_unify_flags ()) clenv gl =
   let concl = Goal.V82.concl clenv.evd (sig_it gl) in
+  let concl = EConstr.Unsafe.to_constr concl in
   if isMeta (fst (decompose_appvect (whd_nored clenv.evd (EConstr.of_constr clenv.templtyp.rebus)))) then
     clenv_unify CUMUL ~flags (clenv_type clenv) concl
       (clenv_unify_meta_types ~flags clenv)
diff --git a/proofs/goal.ml b/proofs/goal.ml
index bcb14e2d6c..4c598ca29e 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -62,6 +62,7 @@ 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.future_goals evars in
     let prev_principal_goal = Evd.principal_future_goal evars in
     let evi = { Evd.evar_hyps = hyps;
@@ -78,13 +79,14 @@ module V82 = struct
     let evars = Sigma.to_evar_map evars in
     let evars = Evd.restore_future_goals evars prev_future_goals prev_principal_goal in
     let ctxt = Environ.named_context_of_val hyps in
-    let inst = Array.map_of_list (NamedDecl.get_id %> mkVar) ctxt in
-    let ev = Term.mkEvar (evk,inst) in
+    let inst = Array.map_of_list (NamedDecl.get_id %> EConstr.mkVar) ctxt in
+    let ev = EConstr.mkEvar (evk,inst) in
     (evk, ev, evars)
 
   (* Instantiates a goal with an open term *)
   let partial_solution sigma evk c =
     (* Check that the goal itself does not appear in the refined term *)
+    let c = EConstr.Unsafe.to_constr c in
     let _ =
       if not (Evarutil.occur_evar_upto sigma evk c) then ()
       else Pretype_errors.error_occur_check Environ.empty_env sigma evk (EConstr.of_constr c)
@@ -158,4 +160,6 @@ module V82 = struct
 					    t
 				       ) ~init:(concl sigma gl) env
 
+  let concl sigma gl = EConstr.of_constr (concl sigma gl)
+
 end
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 6a79c1f451..ca6584e76d 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -38,7 +38,7 @@ module V82 : sig
   val nf_hyps : Evd.evar_map -> goal -> Environ.named_context_val
 
   (* Access to ".evar_concl" *)
-  val concl : Evd.evar_map -> goal -> Term.constr
+  val concl : Evd.evar_map -> goal -> EConstr.constr
 
   (* Access to ".evar_extra" *)
   val extra : Evd.evar_map -> goal -> Evd.Store.t
@@ -48,16 +48,16 @@ module V82 : sig
        the evar corresponding to the goal, and an updated evar_map. *)
   val mk_goal : Evd.evar_map -> 
                          Environ.named_context_val ->
-                         Term.constr ->
+                         EConstr.constr ->
                          Evd.Store.t ->
-                         goal * Term.constr * Evd.evar_map
+                         goal * EConstr.constr * Evd.evar_map
 
   (* Instantiates a goal with an open term *)
-  val partial_solution : Evd.evar_map -> goal -> Term.constr -> Evd.evar_map
+  val partial_solution : Evd.evar_map -> goal -> EConstr.constr -> Evd.evar_map
 
   (* Instantiates a goal with an open term, reusing name of goal for
      second goal *)
-  val partial_solution_to : Evd.evar_map -> goal -> goal -> Term.constr -> Evd.evar_map
+  val partial_solution_to : Evd.evar_map -> goal -> goal -> EConstr.constr -> Evd.evar_map
 
   (* Principal part of the weak-progress tactical *)
   val weak_progress : goal list Evd.sigma -> goal Evd.sigma -> bool
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 093d949d5d..c5d6e3e083 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -349,7 +349,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	let conclty = nf_betaiota sigma (EConstr.of_constr conclty) in
 	  if !check && occur_meta sigma (EConstr.of_constr conclty) then
 	    raise (RefinerError (MetaInType conclty));
-	  let (gl,ev,sigma) = mk_goal hyps conclty in
+	  let (gl,ev,sigma) = mk_goal hyps (EConstr.of_constr conclty) in
+	  let ev = EConstr.Unsafe.to_constr ev in
 	  gl::goalacc, conclty, sigma, ev
 
       | Cast (t,k, ty) ->
@@ -424,7 +425,8 @@ and mk_hdgoals sigma goal goalacc trm =
   match kind_of_term trm with
     | Cast (c,_, ty) when isMeta c ->
 	check_typability env sigma ty;
-	let (gl,ev,sigma) = mk_goal hyps (nf_betaiota sigma (EConstr.of_constr ty)) in
+	let (gl,ev,sigma) = mk_goal hyps (EConstr.of_constr (nf_betaiota sigma (EConstr.of_constr ty))) in
+	let ev = EConstr.Unsafe.to_constr ev in
 	gl::goalacc,ty,sigma,ev
 
     | Cast (t,_, ty) ->
@@ -526,6 +528,7 @@ let prim_refiner r sigma goal =
   let env = Goal.V82.env sigma goal in
   let sign = Goal.V82.hyps sigma goal in
   let cl = Goal.V82.concl sigma goal in
+  let cl = EConstr.Unsafe.to_constr cl in
   let mk_goal hyps concl = 
     Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) 
   in
@@ -533,7 +536,7 @@ let prim_refiner r sigma goal =
     (* Logical rules *)
     | Cut (b,replace,id,t) ->
 (*        if !check && not (Retyping.get_sort_of env sigma t) then*)
-        let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma (EConstr.of_constr t)) in
+        let (sg1,ev1,sigma) = mk_goal sign (EConstr.of_constr (nf_betaiota sigma (EConstr.of_constr t))) in
 	let sign,t,cl,sigma =
 	  if replace then
 	    let nexthyp = get_hyp_after id (named_context_of_val sign) in
@@ -546,9 +549,10 @@ let prim_refiner r sigma goal =
 	      user_err ~hdr:"Logic.prim_refiner"
                 (str "Variable " ++ pr_id id ++ str " is already declared.");
 	     push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in
+        let t = EConstr.of_constr t in
         let (sg2,ev2,sigma) = 
-	  Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
-	let oterm = Term.mkNamedLetIn id ev1 t ev2 in
+	  Goal.V82.mk_goal sigma sign (EConstr.of_constr cl) (Goal.V82.extra sigma goal) in
+	let oterm = EConstr.mkLetIn (Name id, ev1, t, EConstr.Vars.subst_var id ev2) in
 	let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in
         if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
 
@@ -556,5 +560,5 @@ let prim_refiner r sigma goal =
 	check_meta_variables c;
 	let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in
 	let sgl = List.rev sgl in
-	let sigma = Goal.V82.partial_solution sigma goal oterm in
+	let sigma = Goal.V82.partial_solution sigma goal (EConstr.of_constr oterm) in
 	  (sgl, sigma)
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 5e9c0ba8e6..c2ebb76d7a 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -41,7 +41,7 @@ let project  = Refiner.project
 let pf_env   = Refiner.pf_env
 let pf_hyps  = Refiner.pf_hyps
 
-let pf_concl gls = Goal.V82.concl (project gls) (sig_it gls)
+let pf_concl gls = EConstr.Unsafe.to_constr (Goal.V82.concl (project gls) (sig_it gls))
 let pf_hyps_types gls  =
   let sign = Environ.named_context (pf_env gls) in
   List.map (function LocalAssum (id,x)
@@ -137,7 +137,7 @@ open Pp
 let db_pr_goal sigma g =
   let env = Goal.V82.env sigma g in
   let penv = print_named_context env in
-  let pc = print_constr_env env (Goal.V82.concl sigma g) in
+  let pc = print_constr_env env (EConstr.Unsafe.to_constr (Goal.V82.concl sigma g)) in
   str"  " ++ hv 0 (penv ++ fnl () ++
                    str "============================" ++ fnl ()  ++
                    str" "  ++ pc) ++ fnl ()
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index bc1d0ed6b3..be8d7eaa5f 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -185,7 +185,7 @@ let set_typeclasses_depth =
 
 let pr_ev evs ev =
   Printer.pr_constr_env (Goal.V82.env evs ev) evs
-                        (Evarutil.nf_evar evs (Goal.V82.concl evs ev))
+                        (Evarutil.nf_evar evs (EConstr.Unsafe.to_constr (Goal.V82.concl evs ev)))
 
 (** Typeclasses instance search tactic / eauto *)
 
@@ -672,6 +672,7 @@ module V85 = struct
   let hints_tac hints sk fk {it = gl,info; sigma = s} =
     let env = Goal.V82.env s gl in
     let concl = Goal.V82.concl s gl in
+    let concl = EConstr.Unsafe.to_constr concl in
     let tacgl = {it = gl; sigma = s;} in
     let secvars = secvars_of_hyps (Environ.named_context_of_val (Goal.V82.hyps s gl)) in
     let poss = e_possible_resolve hints info.hints secvars info.only_classes s concl in
@@ -784,7 +785,7 @@ module V85 = struct
                  let fk'' =
                    if not info.unique && List.is_empty gls' &&
                         not (needs_backtrack (Goal.V82.env s gl) s
-                                           info.is_evar (Goal.V82.concl s gl))
+                                           info.is_evar (EConstr.Unsafe.to_constr (Goal.V82.concl s gl)))
                    then fk
                    else fk'
                  in
@@ -1458,7 +1459,7 @@ let _ =
 let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
   let nc, gl, subst, _, _ = Evarutil.push_rel_context_to_named_context env gl in
   let (gl,t,sigma) =
-    Goal.V82.mk_goal sigma nc (EConstr.Unsafe.to_constr gl) Store.empty in
+    Goal.V82.mk_goal sigma nc gl Store.empty in
   let gls = { it = gl ; sigma = sigma; } in
   let hints = searchtable_map typeclasses_db in
   let st = Hint_db.transparent_state hints in
@@ -1473,6 +1474,7 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl unique =
       with Refiner.FailError _ -> raise Not_found
   in
   let evd = sig_sig gls' in
+  let t = EConstr.Unsafe.to_constr t in
   let t' = let (ev, inst) = destEvar t in
     mkEvar (ev, Array.of_list subst)
   in
diff --git a/tactics/hints.ml b/tactics/hints.ml
index e8225df2d0..57358bb769 100644
--- a/tactics/hints.ml
+++ b/tactics/hints.ml
@@ -1423,7 +1423,7 @@ let pr_applicable_hint () =
   match glss.Evd.it with
   | [] -> CErrors.error "No focused goal."
   | g::_ ->
-    pr_hint_term glss.Evd.sigma (Goal.V82.concl glss.Evd.sigma g)
+    pr_hint_term glss.Evd.sigma (EConstr.Unsafe.to_constr (Goal.V82.concl glss.Evd.sigma g))
 
 let pp_hint_mode = function
   | ModeInput -> str"+"