Goal: remove some functions from the compatibility layer.

The rest will take more work.

5 files changed, 10 insertions, 56 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 544282c4d..7a69a6035 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -55,11 +55,6 @@ module V82 = struct
     let evi = Evd.find evars gl in
     Evd.evar_filtered_env evi
 
-  (* same as [env], but ensures that existential variables are
-     normalised *)
-  let nf_env evars gl =
-    Evarutil.nf_env_evar evars (env evars gl)
-
   (* Old style hyps primitive *)
   let hyps evars gl =
     let evi = Evd.find evars gl in
@@ -76,21 +71,11 @@ module V82 = struct
     let evi = Evd.find evars gl in
     evi.Evd.evar_concl
 
-  (* same as [concl] but ensures that existential variables are
-     normalised. *)
-  let nf_concl evars gl =
-    Evarutil.nf_evar evars (concl evars gl)
-
   (* Access to ".evar_extra" *)
   let extra evars gl =
     let evi = Evd.find evars gl in
     evi.Evd.evar_extra
 
-  (* Old style filtered_context primitive *)
-  let filtered_context evars gl =
-    let evi = Evd.find evars gl in
-    Evd.evar_filtered_context evi
-
   (* Old style mk_goal primitive *)
   let mk_goal evars hyps concl extra =
     let evi = { Evd.evar_hyps = hyps;
@@ -108,18 +93,6 @@ module V82 = struct
     let ev = Term.mkEvar (evk,inst) in
     (evk, ev, evars)
 
-  (* Creates a dummy [goal sigma] for use in auto *)
-  let dummy_goal =
-    (* This goal seems to be marshalled somewhere. Therefore it cannot be
-       marked unresolvable for typeclasses, as non-empty Store.t-s happen
-       to have functional content. *)
-    let evi = Evd.make_evar Environ.empty_named_context_val Term.mkProp in
-    let (sigma, evk) = Evarutil.new_pure_evar_full Evd.empty evi in
-    { Evd.it = evk ; Evd.sigma = sigma; }
-
-  (* Makes a goal out of an evar *)
-  let build e = e
-
   (* Instantiates a goal with an open term *)
   let partial_solution sigma evk c =
     Evd.define evk c sigma
@@ -150,7 +123,7 @@ module V82 = struct
        with a good implementation of them.
     *)
 
-  (* Used for congruence closure and change *)
+  (* Used for congruence closure  *)
   let new_goal_with sigma gl extra_hyps =
     let evi = Evd.find sigma gl in
     let hyps = evi.Evd.evar_hyps in
@@ -162,7 +135,7 @@ module V82 = struct
       { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in
     let new_evi = Typeclasses.mark_unresolvable new_evi in
     let (new_sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in
-    { Evd.it = build evk ; sigma = new_sigma; }
+    { Evd.it = evk ; sigma = new_sigma; }
 
   (* Used by the compatibility layer and typeclasses *)
   let nf_evar sigma gl =
diff --git a/proofs/goal.mli b/proofs/goal.mli
index 7c8fdef29..7a14848b5 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -34,10 +34,6 @@ module V82 : sig
   (* Old style env primitive *)
   val env : Evd.evar_map -> goal -> Environ.env
 
-  (* same as [env], but ensures that existential variables are
-     normalised *)
-  val nf_env : Evd.evar_map -> goal -> Environ.env
-
   (* Old style hyps primitive *)
   val hyps : Evd.evar_map -> goal -> Environ.named_context_val
 
@@ -48,16 +44,9 @@ module V82 : sig
   (* Access to ".evar_concl" *)
   val concl : Evd.evar_map -> goal -> Term.constr
 
-  (* same as [concl] but ensures that existential variables are
-     normalised. *)
-  val nf_concl : Evd.evar_map -> goal -> Term.constr
-
   (* Access to ".evar_extra" *)
   val extra : Evd.evar_map -> goal -> Evd.Store.t
 
-  (* Old style filtered_context primitive *)
-  val filtered_context : Evd.evar_map -> goal -> Context.named_context
-
   (* Old style mk_goal primitive, returns a new goal with corresponding 
        hypotheses and conclusion, together with a term which is precisely
        the evar corresponding to the goal, and an updated evar_map. *)
@@ -67,15 +56,6 @@ module V82 : sig
                          Evd.Store.t ->
                          goal * Term.constr * Evd.evar_map
 
-  (* Creates a dummy [goal sigma] for use in auto *)
-  val dummy_goal : goal Evd.sigma
-
-  (* Makes a goal out of an evar *)
-  (* spiwack: used by [Proofview.init], not entirely clean probably, but it is
-      the only way I could think of to preserve compatibility with previous Coq
-      stuff. *)
-  val build : Evd.evar -> goal 
-
   (* Instantiates a goal with an open term *)
   val partial_solution : Evd.evar_map -> goal -> Term.constr -> Evd.evar_map
 
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index e6c8032bf..30c763ac1 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -851,7 +851,7 @@ module V82 = struct
    { Evd.it = comb ; sigma = solution }
 
   let top_goals initial { solution=solution; } =
-    let goals = List.map (fun (t,_) -> Goal.V82.build (fst (Term.destEvar t))) initial in
+    let goals = List.map (fun (t,_) -> fst (Term.destEvar t)) initial in
     { Evd.it = goals ; sigma=solution; }
 
   let top_evars initial =
@@ -896,8 +896,6 @@ module V82 = struct
 end
 
 type goal = Goal.goal
-let partial_solution = Goal.V82.partial_solution
-let partial_solution_to = Goal.V82.partial_solution_to
 
 module Goal = struct
 
@@ -1022,8 +1020,11 @@ struct
     let sigma = if unsafe then sigma else typecheck_proof c concl env sigma in
     (** Proceed to the refinement *)
     let sigma = match evkmain with
-      | None -> partial_solution sigma gl.Goal.self c 
-      | Some evk -> partial_solution_to sigma gl.Goal.self evk c in
+      | None -> Evd.define gl.Goal.self c sigma
+      | Some evk ->
+          let id = Evd.evar_ident gl.Goal.self sigma in
+          Evd.rename evk id (Evd.define gl.Goal.self c sigma)
+    in
     (** Select the goals *)
     let comb = undefined sigma (List.rev evs) in
     let sigma = List.fold_left mark_as_goal sigma comb in
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 344597fcd..f8bca1155 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -40,7 +40,7 @@ let evars_to_goals p evm =
   let goals = ref Evar.Map.empty in
   let map ev evi =
     let evi, goal = p evm ev evi in
-    let () = if goal then goals := Evar.Map.add ev (Goal.V82.build ev) !goals in
+    let () = if goal then goals := Evar.Map.add ev ev !goals in
     evi
   in
   let evm = Evd.raw_map_undefined map evm in
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index cd460ebbe..f7c3c922f 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -1237,7 +1237,7 @@ and eval_tactic ist tac : unit Proofview.tactic = match tac with
       let env = Environ.empty_env in
       let sigma = Evd.empty in
       let concl = Term.mkRel (-1) in
-      let goal = sig_it Goal.V82.dummy_goal in
+      let goal = Evar.unsafe_of_int (-1) in
       (* /dummy values *)
       let args = List.map (fun a -> snd(interp_genarg ist env sigma concl goal a)) l in
       catch_error_tac trace (tac args ist)