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.

1 files changed, 12 insertions, 12 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 =