diff options
| author | Gaëtan Gilbert | 2017-10-31 17:04:02 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2019-03-14 13:27:38 +0100 |
| commit | 23f84f37c674a07e925925b7e0d50d7ee8414093 (patch) | |
| tree | 7e470de5769c994d8df37c44fed12cf299d5b194 /pretyping/patternops.ml | |
| parent | 75508769762372043387c67a9abe94e8f940e80a (diff) | |
Add relevance marks on binders.
Kernel should be mostly correct, higher levels do random stuff at
times.
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 20 |
1 files changed, 12 insertions, 8 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 305ebf3dd5..13034d078a 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -15,6 +15,7 @@ open Globnames open Nameops open Term open Constr +open Context open Glob_term open Pp open Mod_subst @@ -158,12 +159,15 @@ let pattern_of_constr env sigma t = | Sort Set -> PSort GSet | Sort (Type _) -> PSort (GType []) | Cast (c,_,_) -> pattern_of_constr env c - | LetIn (na,c,t,b) -> PLetIn (na,pattern_of_constr env c,Some (pattern_of_constr env t), - 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 (LocalAssum (na, c)) env) b) - | Lambda (na,c,b) -> PLambda (na,pattern_of_constr env c, - pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) + | LetIn (na,c,t,b) -> PLetIn (na.binder_name, + pattern_of_constr env c,Some (pattern_of_constr env t), + pattern_of_constr (push_rel (LocalDef (na,c,t)) env) b) + | Prod (na,c,b) -> PProd (na.binder_name, + pattern_of_constr env c, + pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) + | Lambda (na,c,b) -> PLambda (na.binder_name, + pattern_of_constr env c, + pattern_of_constr (push_rel (LocalAssum (na, c)) env) b) | App (f,a) -> (match match kind f with @@ -207,12 +211,12 @@ let pattern_of_constr env sigma t = | Fix (lni,(lna,tl,bl)) -> let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in let env' = Array.fold_left2 push env lna tl in - PFix (lni,(lna,Array.map (pattern_of_constr env) tl, + PFix (lni,(Array.map binder_name lna,Array.map (pattern_of_constr env) tl, Array.map (pattern_of_constr env') bl)) | CoFix (ln,(lna,tl,bl)) -> let push env na2 c2 = push_rel (LocalAssum (na2,c2)) env in let env' = Array.fold_left2 push env lna tl in - PCoFix (ln,(lna,Array.map (pattern_of_constr env) tl, + PCoFix (ln,(Array.map binder_name lna,Array.map (pattern_of_constr env) tl, Array.map (pattern_of_constr env') bl)) | Int i -> PInt i in pattern_of_constr env t |