Definining EConstr-based contexts.

This removes quite a few unsafe casts. Unluckily, I had to reintroduce
the old non-module based names for these data structures, because I could
not reproduce easily the same hierarchy in EConstr.

2 files changed, 18 insertions, 16 deletions

diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml
index 475380512..adb11f4f8 100644
--- a/plugins/rtauto/refl_tauto.ml
+++ b/plugins/rtauto/refl_tauto.ml
@@ -66,19 +66,18 @@ let l_E_Or = lazy (constant "E_Or")
 let l_D_Or = lazy (constant "D_Or")
 
 
-let special_whd gl=
-  let infos=CClosure.create_clos_infos CClosure.all (pf_env gl) in
-    (fun t -> CClosure.whd_val infos (CClosure.inject t))
+let special_whd gl c =
+  Reductionops.clos_whd_flags CClosure.all (pf_env gl) (Tacmach.project gl) c
 
-let special_nf gl=
-  let infos=CClosure.create_clos_infos CClosure.betaiotazeta (pf_env gl) in
-    (fun t -> CClosure.norm_val infos (CClosure.inject t))
+let special_nf gl c =
+  Reductionops.clos_norm_flags CClosure.betaiotazeta (pf_env gl) (Tacmach.project gl) c
 
 type atom_env=
     {mutable next:int;
      mutable env:(constr*int) list}
 
 let make_atom atom_env term=
+  let term = EConstr.Unsafe.to_constr term in
   try
     let (_,i)=
       List.find (fun (t,_)-> eq_constr term t) atom_env.env
@@ -90,13 +89,17 @@ let make_atom atom_env term=
       Atom i
 
 let rec make_form atom_env gls term =
+  let open EConstr in
+  let open Vars in
   let normalize=special_nf gls in
   let cciterm=special_whd gls term  in
-    match kind_of_term cciterm with
+  let sigma = Tacmach.project gls in
+  let inj = EConstr.Unsafe.to_constr in
+    match EConstr.kind sigma cciterm with
 	Prod(_,a,b) ->
-	  if EConstr.Vars.noccurn (Tacmach.project gls) 1 (EConstr.of_constr b) &&
+	  if noccurn sigma 1 b &&
 	    Retyping.get_sort_family_of
-	    (pf_env gls) (Tacmach.project gls) (EConstr.of_constr a) == InProp
+	    (pf_env gls) sigma a == InProp
 	  then
 	    let fa=make_form atom_env gls a in
 	    let fb=make_form atom_env gls b in
@@ -113,7 +116,7 @@ let rec make_form atom_env gls term =
       | App(hd,argv) when Int.equal (Array.length argv) 2 ->
 	  begin
 	    try
-	      let ind, _ = destInd hd in
+	      let ind, _ = destInd sigma hd in
 		if Names.eq_ind ind (fst (Lazy.force li_and)) then
 		  let fa=make_form atom_env gls argv.(0) in
 		  let fb=make_form atom_env gls argv.(1) in
@@ -134,9 +137,9 @@ let rec make_hyps atom_env gls lenv = function
   | LocalAssum (id,typ)::rest ->
       let hrec=
 	make_hyps atom_env gls (typ::lenv) rest in
-	if List.exists (fun c -> Termops.local_occur_var Evd.empty (** FIXME *) id (EConstr.of_constr c)) lenv ||
+	if List.exists (fun c -> Termops.local_occur_var Evd.empty (** FIXME *) id c) lenv ||
 	  (Retyping.get_sort_family_of
-	     (pf_env gls) (Tacmach.project gls) (EConstr.of_constr typ) != InProp)
+	     (pf_env gls) (Tacmach.project gls) typ != InProp)
 	then
 	  hrec
 	else
@@ -264,7 +267,6 @@ let rtauto_tac gls=
     if Retyping.get_sort_family_of
       (pf_env gls) (Tacmach.project gls) gl != InProp
     then user_err ~hdr:"rtauto" (Pp.str "goal should be in Prop") in
-  let gl = EConstr.Unsafe.to_constr gl in
   let glf=make_form gamma gls gl in
   let hyps=make_hyps gamma gls [gl] (pf_hyps gls) in
   let formula=
diff --git a/plugins/rtauto/refl_tauto.mli b/plugins/rtauto/refl_tauto.mli
index 9a14ac6c7..092552364 100644
--- a/plugins/rtauto/refl_tauto.mli
+++ b/plugins/rtauto/refl_tauto.mli
@@ -12,13 +12,13 @@ type atom_env=
      mutable env:(Term.constr*int) list}
 
 val make_form : atom_env ->
-    Proof_type.goal Tacmach.sigma -> Term.types -> Proof_search.form
+    Proof_type.goal Tacmach.sigma -> EConstr.types -> Proof_search.form
 
 val make_hyps :
     atom_env ->
     Proof_type.goal Tacmach.sigma ->
-    Term.types list ->
-    Context.Named.t ->
+    EConstr.types list ->
+    EConstr.named_context ->
     (Names.Id.t * Proof_search.form) list
 
 val rtauto_tac : Proof_type.tactic