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.

1 files changed, 4 insertions, 13 deletions

diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 26e23be23c..954aa6a94c 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -121,19 +121,10 @@ let head_of_constr_reference sigma c = match EConstr.kind sigma c with
   | Var id -> VarRef id
   | _ -> anomaly (Pp.str "Not a rigid reference")
 
-let local_assum (na, t) =
-  let open Context.Rel.Declaration in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalAssum (na, inj t)
-
-let local_def (na, b, t) =
-  let open Context.Rel.Declaration in
-  let inj = EConstr.Unsafe.to_constr in
-  LocalDef (na, inj b, inj t)
-
 let pattern_of_constr env sigma t =
   let open EConstr in
   let rec pattern_of_constr env t =
+  let open Context.Rel.Declaration in
   match EConstr.kind sigma t with
     | Rel n  -> PRel n
     | Meta n -> PMeta (Some (Id.of_string ("META" ^ string_of_int n)))
@@ -143,11 +134,11 @@ let pattern_of_constr env sigma t =
     | Sort (Type _) -> PSort (GType [])
     | Cast (c,_,_)      -> pattern_of_constr env c
     | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,
-				  pattern_of_constr (push_rel (local_def (na,c,t)) env) b)
+				  pattern_of_constr (push_rel (LocalDef (na,c,t)) env) b)
     | Prod (na,c,b)   -> PProd (na,pattern_of_constr env c,
-				pattern_of_constr (push_rel (local_assum (na, c)) env) b)
+				pattern_of_constr (push_rel (LocalAssum (na, c)) env) b)
     | Lambda (na,c,b) -> PLambda (na,pattern_of_constr env c,
-				  pattern_of_constr (push_rel (local_assum (na, c)) env) b)
+				  pattern_of_constr (push_rel (LocalAssum (na, c)) env) b)
     | App (f,a) ->
         (match
           match EConstr.kind sigma f with