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.

7 files changed, 28 insertions, 21 deletions

diff --git a/proofs/goal.ml b/proofs/goal.ml
index 410e738de..9046f4534 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -155,6 +155,7 @@ module V82 = struct
       with Not_found -> true in
     Environ.fold_named_context_reverse (fun t decl ->
 					  if is_proof_var decl then
+                                            let decl = Termops.map_named_decl EConstr.of_constr decl in
 					    mkNamedProd_or_LetIn decl t
 					  else
 					    t
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 59ce8ffa6..a31cadd88 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -174,12 +174,14 @@ let reorder_context env sigma sign ord =
   step ord ords sign mt_q []
 
 let reorder_val_context env sigma sign ord =
+  let open EConstr in
   val_of_named_context (reorder_context env sigma (named_context_of_val sign) ord)
 
 
 
 
 let check_decl_position env sigma sign d =
+  let open EConstr in
   let x = NamedDecl.get_id d in
   let needed = global_vars_set_of_decl env sigma d in
   let deps = dependency_closure env sigma (named_context_of_val sign) needed in
@@ -266,6 +268,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto =
       	else
 	  moverec first' middle' right
   in
+  let open EConstr in
   if toleft then
     let right =
       List.fold_right push_named_context_val right empty_named_context_val in
@@ -279,6 +282,7 @@ let move_hyp sigma toleft (left,declfrom,right) hto =
       right left
 
 let move_hyp_in_named_context sigma hfrom hto sign =
+  let open EConstr in
   let (left,right,declfrom,toleft) =
     split_sign hfrom hto (named_context_of_val sign) in
   move_hyp sigma toleft (left,declfrom,right) hto
@@ -507,7 +511,7 @@ and mk_casegoals sigma goal goalacc p c =
 
 let convert_hyp check sign sigma d =
   let id = NamedDecl.get_id d in
-  let b = Option.map EConstr.of_constr (NamedDecl.get_value d) in
+  let b = NamedDecl.get_value d in
   let env = Global.env() in
   let reorder = ref [] in
   let sign' =
@@ -515,14 +519,14 @@ let convert_hyp check sign sigma d =
       (fun _ d' _ ->
         let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in
         let env = Global.env_of_context sign in
-        if check && not (is_conv env sigma (EConstr.of_constr (NamedDecl.get_type d)) (EConstr.of_constr (NamedDecl.get_type d'))) then
+        if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then
 	  user_err ~hdr:"Logic.convert_hyp"
             (str "Incorrect change of the type of " ++ pr_id id ++ str ".");
         if check && not (Option.equal (is_conv env sigma) b c) then
 	  user_err ~hdr:"Logic.convert_hyp"
             (str "Incorrect change of the body of "++ pr_id id ++ str ".");
        if check then reorder := check_decl_position env sigma sign d;
-       d) in
+       map_named_decl EConstr.Unsafe.to_constr d) in
   reorder_val_context env sigma sign' !reorder
 
 
@@ -535,15 +539,16 @@ let prim_refiner r sigma goal =
   let env = Goal.V82.env sigma goal in
   let sign = Goal.V82.hyps sigma goal in
   let cl = Goal.V82.concl sigma goal in
-  let cl = EConstr.Unsafe.to_constr cl in
   let mk_goal hyps concl = 
     Goal.V82.mk_goal sigma hyps concl (Goal.V82.extra sigma goal) 
   in
+  let open EConstr in
   match r with
     (* Logical rules *)
     | Cut (b,replace,id,t) ->
 (*        if !check && not (Retyping.get_sort_of env sigma t) then*)
-        let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma (EConstr.of_constr t)) in
+        let t = EConstr.of_constr t in
+        let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in
 	let sign,t,cl,sigma =
 	  if replace then
 	    let nexthyp = get_hyp_after id (named_context_of_val sign) in
@@ -556,14 +561,14 @@ let prim_refiner r sigma goal =
 	      user_err ~hdr:"Logic.prim_refiner"
                 (str "Variable " ++ pr_id id ++ str " is already declared.");
 	     push_named_context_val (LocalAssum (id,t)) sign,t,cl,sigma) in
-        let t = EConstr.of_constr t in
         let (sg2,ev2,sigma) = 
-	  Goal.V82.mk_goal sigma sign (EConstr.of_constr cl) (Goal.V82.extra sigma goal) in
-	let oterm = EConstr.mkLetIn (Name id, ev1, t, EConstr.Vars.subst_var id ev2) in
+	  Goal.V82.mk_goal sigma sign cl (Goal.V82.extra sigma goal) in
+	let oterm = mkLetIn (Name id, ev1, t, EConstr.Vars.subst_var id ev2) in
 	let sigma = Goal.V82.partial_solution_to sigma goal sg2 oterm in
         if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
 
     | Refine c ->
+        let cl = EConstr.Unsafe.to_constr cl in
 	check_meta_variables c;
 	let (sgl,cl',sigma,oterm) = mk_refgoals sigma goal [] cl c in
 	let sgl = List.rev sgl in
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 5fe28ac76..f98248e4d 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -55,7 +55,7 @@ exception RefinerError of refiner_error
 val catchable_exception : exn -> bool
 
 val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
-  Context.Named.Declaration.t -> Environ.named_context_val
+  EConstr.named_declaration -> Environ.named_context_val
 
 val move_hyp_in_named_context : Evd.evar_map -> Id.t -> Id.t Misctypes.move_location ->
   Environ.named_context_val -> Environ.named_context_val
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 9a0b56b84..5c7659ac0 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -22,7 +22,7 @@ let project x = x.sigma
 (* Getting env *)
 
 let pf_env gls = Global.env_of_context (Goal.V82.hyps (project gls) (sig_it gls))
-let pf_hyps gls = named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls))
+let pf_hyps gls = EConstr.named_context_of_val (Goal.V82.hyps (project gls) (sig_it gls))
 
 let refiner pr goal_sigma =
   let (sgl,sigma') = prim_refiner pr goal_sigma.sigma goal_sigma.it in
@@ -198,10 +198,10 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
    destruct), this is not detected by this tactical. *)
 let tclSHOWHYPS (tac : tactic) (goal: Goal.goal Evd.sigma)
     :Proof_type.goal list Evd.sigma =
-  let oldhyps:Context.Named.t = pf_hyps goal in
+  let oldhyps = pf_hyps goal in
   let rslt:Proof_type.goal list Evd.sigma = tac goal in
   let { it = gls; sigma = sigma; } = rslt in
-  let hyps:Context.Named.t list =
+  let hyps =
     List.map (fun gl -> pf_hyps { it = gl; sigma=sigma; }) gls in
   let cmp d1 d2 = Names.Id.equal (NamedDecl.get_id d1) (NamedDecl.get_id d2) in
   let newhyps =
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 6dcafb77a..56f5facf8 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -10,6 +10,7 @@
 
 open Evd
 open Proof_type
+open EConstr
 
 (** The refiner (handles primitive rules and high-level tactics). *)
 
@@ -17,7 +18,7 @@ val sig_it  : 'a sigma -> 'a
 val project : 'a sigma -> evar_map
 
 val pf_env  : goal sigma -> Environ.env
-val pf_hyps : goal sigma -> Context.Named.t
+val pf_hyps : goal sigma -> named_context
 
 val unpackage : 'a sigma -> evar_map ref * 'a
 val repackage : evar_map ref -> 'a -> 'a sigma
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 3ed262d6e..4b027a127 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -64,7 +64,7 @@ let pf_get_hyp gls id =
     raise (RefinerError (NoSuchHyp id))
 
 let pf_get_hyp_typ gls id =
-  id |> pf_get_hyp gls |> NamedDecl.get_type |> EConstr.of_constr
+  id |> pf_get_hyp gls |> NamedDecl.get_type
 
 let pf_ids_of_hyps gls = ids_of_named_context (pf_hyps gls)
 
@@ -199,13 +199,13 @@ module New = struct
   let pf_get_hyp id gl =
     let hyps = Proofview.Goal.env gl in
     let sign =
-      try Environ.lookup_named id hyps
+      try EConstr.lookup_named id hyps
       with Not_found -> raise (RefinerError (NoSuchHyp id))
     in
     sign
 
   let pf_get_hyp_typ id gl =
-    pf_get_hyp id gl |> NamedDecl.get_type |> EConstr.of_constr
+    pf_get_hyp id gl |> NamedDecl.get_type
 
   let pf_hyps_types gl =
     let env = Proofview.Goal.env gl in
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index efc3dbf55..3b23a6ab4 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -34,18 +34,18 @@ val apply_sig_tac :
 
 val pf_concl              : goal sigma -> types
 val pf_env                : goal sigma -> env
-val pf_hyps               : goal sigma -> Context.Named.t
+val pf_hyps               : goal sigma -> named_context
 (*i val pf_untyped_hyps       : goal sigma -> (Id.t * constr) list i*)
 val pf_hyps_types         : goal sigma -> (Id.t * types) list
 val pf_nth_hyp_id         : goal sigma -> int -> Id.t
-val pf_last_hyp           : goal sigma -> Context.Named.Declaration.t
+val pf_last_hyp           : goal sigma -> named_declaration
 val pf_ids_of_hyps        : goal sigma -> Id.t list
 val pf_global             : goal sigma -> Id.t -> constr
 val pf_unsafe_type_of            : goal sigma -> constr -> types
 val pf_type_of            : goal sigma -> constr -> evar_map * types
 val pf_hnf_type_of        : goal sigma -> constr -> types
 
-val pf_get_hyp            : goal sigma -> Id.t -> Context.Named.Declaration.t
+val pf_get_hyp            : goal sigma -> Id.t -> named_declaration
 val pf_get_hyp_typ        : goal sigma -> Id.t -> types
 
 val pf_get_new_id  : Id.t      -> goal sigma -> Id.t
@@ -117,9 +117,9 @@ module New : sig
   val pf_ids_of_hyps : ('a, 'r) Proofview.Goal.t -> identifier list
   val pf_hyps_types : ('a, 'r) Proofview.Goal.t -> (identifier * types) list
 
-  val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t
+  val pf_get_hyp : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> named_declaration
   val pf_get_hyp_typ        : identifier -> ([ `NF ], 'r) Proofview.Goal.t -> types
-  val pf_last_hyp           : ([ `NF ], 'r) Proofview.Goal.t -> Context.Named.Declaration.t
+  val pf_last_hyp           : ([ `NF ], 'r) Proofview.Goal.t -> named_declaration
 
   val pf_nf_concl : ([ `LZ ], 'r) Proofview.Goal.t -> types
   val pf_reduce_to_quantified_ind : ('a, 'r) Proofview.Goal.t -> types -> pinductive * types