diff options
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 17 |
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 |