From 9ebf44d84754adc5b64fcf612c6816c02c80462d Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 2 Feb 2019 19:29:23 -0500
Subject: Imported Upstream version 8.9.0

---
 proofs/goal.ml | 25 +++++++------------------
 1 file changed, 7 insertions(+), 18 deletions(-)

(limited to 'proofs/goal.ml')

diff --git a/proofs/goal.ml b/proofs/goal.ml
index ba7e458f..c14c0a8a 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 =
@@ -117,20 +118,6 @@ module V82 = struct
        with a good implementation of them.
     *)
 
-  (* 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
-    let new_hyps =
-      List.fold_right Environ.push_named_context_val extra_hyps hyps in
-    let filter = evi.Evd.evar_filter in
-    let new_filter = Evd.Filter.extend (List.length extra_hyps) filter in
-    let new_evi =
-      { evi with Evd.evar_hyps = new_hyps; Evd.evar_filter = new_filter } in
-    let new_evi = Typeclasses.mark_unresolvable new_evi in
-    let (sigma, evk) = Evarutil.new_pure_evar_full Evd.empty new_evi in
-    { Evd.it = evk ; sigma = sigma; }
-
   (* Used by the compatibility layer and typeclasses *)
   let nf_evar sigma gl =
     let evi = Evd.find sigma gl in
@@ -156,3 +143,5 @@ module V82 = struct
 				       ) ~init:(concl sigma gl) env
 
 end
+
+module Set = Set.Make(struct type t = goal let compare = Evar.compare end)
-- 
cgit v1.2.3