diff options
| author | Maxime Dénès | 2018-02-12 09:59:16 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2018-02-12 09:59:16 +0100 |
| commit | 4fb4f1adf18648b4fb561986379e033b00423148 (patch) | |
| tree | 876f561f9310b9e15f3ac20ca71f9dd28f90b157 /pretyping/patternops.ml | |
| parent | 349944eb8e3abd51dc2b94051a887253a2ae9198 (diff) | |
| parent | de988641848ecb26f749fbc3f50ce9194db46a4c (diff) | |
Merge PR #6651: Use r.(p) syntax to print primitive projections.
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 41e09004c6..1bec4a6f15 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -137,8 +137,7 @@ let rec head_pattern_bound t = | PCase (_,p,c,br) -> head_pattern_bound c | PRef r -> r | PVar id -> VarRef id - | PProj (p,c) -> ConstRef (Projection.constant p) - | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ + | PEvar _ | PRel _ | PMeta _ | PSoApp _ | PSort _ | PFix _ | PProj _ -> raise BoundPattern (* Perhaps they were arguments, but we don't beta-reduce *) | PLambda _ -> raise BoundPattern @@ -446,6 +445,9 @@ let rec pat_of_raw metas vars = DAst.with_loc_val (fun ?loc -> function one non-trivial branch. These facts are used in [Constrextern]. *) PCase (info, pred, pat_of_raw metas vars c, brs) + | GProj(p,c) -> + PProj(p, pat_of_raw metas vars c) + | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ -> err ?loc (Pp.str "Non supported pattern.")) |