From 0ae6d27680e5b87bbb00c6941cee1b0c309624ec Mon Sep 17 00:00:00 2001
From: Arnaud Spiwack <arnaud@spiwack.net>
Date: Mon, 13 Oct 2014 18:26:05 +0200
Subject: Goal: remove some functions from the compatibility layer.

The rest will take more work.
---
 proofs/goal.ml | 31 ++-----------------------------
 1 file changed, 2 insertions(+), 29 deletions(-)

(limited to 'proofs/goal.ml')

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 =
-- 
cgit v1.2.3