Congruence: getting rid of a detour by the compatibility layer of proof engine.

The V82 compatibility layer of the proof engine was used by cc
(congruence closure) for the sole purpose of maintaining an
environment and a sigma. We inline the corresponding env and sigma in
the state of cc algorithm to get rid of the compatibility layer.

3 files changed, 12 insertions, 29 deletions

diff --git a/plugins/cc/ccalgo.ml b/plugins/cc/ccalgo.ml
index 5a4818926..5cab6d203 100644
--- a/plugins/cc/ccalgo.ml
+++ b/plugins/cc/ccalgo.ml
@@ -18,7 +18,6 @@ open Names
 open Sorts
 open Constr
 open Vars
-open Evd
 open Goptions
 open Tacmach
 open Util
@@ -272,7 +271,8 @@ type state =
      mutable rew_depth:int;
      mutable changed:bool;
      by_type: Int.Set.t Typehash.t;
-     mutable gls:Goal.goal Evd.sigma}
+     mutable env:Environ.env;
+     sigma:Evd.evar_map}
 
 let dummy_node =
   {
@@ -307,7 +307,8 @@ let empty depth gls:state =
     rew_depth=depth;
     by_type=Constrhash.create init_size;
     changed=false;
-    gls=gls
+    env=pf_env gls;
+    sigma=project gls
   }
     
 let forest state = state.uf
@@ -511,8 +512,8 @@ let rec add_term state t=
 	Not_found ->
 	  let b=next uf in
           let trm = constr_of_term t in
-	  let typ = pf_unsafe_type_of state.gls (EConstr.of_constr trm) in
-	  let typ = canonize_name (project state.gls) typ in
+          let typ = Typing.unsafe_type_of state.env state.sigma (EConstr.of_constr trm) in
+          let typ = canonize_name state.sigma typ in
 	  let new_node=
 	    match t with
 		Symb _ | Product (_,_) ->
@@ -820,11 +821,10 @@ let one_step state =
 let __eps__ = Id.of_string "_eps_"
 
 let new_state_var typ state =
-  let id = pf_get_new_id __eps__ state.gls in
-  let {it=gl ; sigma=sigma} = state.gls in
-  let gls = Goal.V82.new_goal_with sigma gl [Context.Named.Declaration.LocalAssum (id,typ)] in
-    state.gls<- gls;
-    id
+  let ids = Environ.ids_of_named_context_val (Environ.named_context_val state.env) in
+  let id = Namegen.next_ident_away __eps__ ids in
+  state.env<- EConstr.push_named (Context.Named.Declaration.LocalAssum (id,typ)) state.env;
+  id
 
 let complete_one_class state i=
   match (get_representative state.uf i).inductive_status with
@@ -832,9 +832,9 @@ let complete_one_class state i=
 	let rec app t typ n =
 	  if n<=0 then t else
 	    let _,etyp,rest= destProd typ in
-	    let id = new_state_var etyp state in
+            let id = new_state_var (EConstr.of_constr etyp) state in
 		app (Appli(t,Eps id)) (substl [mkVar id] rest) (n-1) in
-	let _c = pf_unsafe_type_of state.gls
+        let _c = Typing.unsafe_type_of state.env state.sigma
 	  (EConstr.of_constr (constr_of_term (term state.uf pac.cnode))) in
         let _c = EConstr.Unsafe.to_constr _c in
 	let _args =
diff --git a/proofs/goal.ml b/proofs/goal.ml
index ba7e458f3..6912db364 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -117,20 +117,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
diff --git a/proofs/goal.mli b/proofs/goal.mli
index dc9863156..b8c979ad7 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -64,9 +64,6 @@ module V82 : sig
  (* Principal part of tclNOTSAMEGOAL *)
   val same_goal : Evd.evar_map -> goal -> Evd.evar_map -> goal -> bool
 
- (* Used for congruence closure *)
-  val new_goal_with : Evd.evar_map -> goal -> Context.Named.t -> goal Evd.sigma
-
   (* Used by the compatibility layer and typeclasses *)
   val nf_evar : Evd.evar_map -> goal -> goal * Evd.evar_map