From b4b90c5d2e8c413e1981c456c933f35679386f09 Mon Sep 17 00:00:00 2001
From: Pierre-Marie Pédrot
Date: Sat, 26 Nov 2016 16:18:47 +0100
Subject: 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.
---
 pretyping/patternops.ml | 17 ++++-------------
 1 file changed, 4 insertions(+), 13 deletions(-)

(limited to 'pretyping/patternops.ml')

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
-- 
cgit v1.2.3