diff options
| author | Maxime Dénès | 2017-03-16 13:24:03 +0100 |
|---|---|---|
| committer | Maxime Dénès | 2017-11-23 18:15:24 +0100 |
| commit | 39cbf75c554cd7e5228bd6cd962766e865c3f26b (patch) | |
| tree | c434651d7d17b9e268b053a40b676009189aca5b /pretyping/patternops.ml | |
| parent | 22ae762fa8940028f6a3d8a5fd4147d5ca3b53b9 (diff) | |
Make some functions on terms more robust w.r.t new term constructs.
Extending terms is notoriously difficult. We try to get more help from
the compiler by making sure such an extension will trigger non
exhaustive pattern matching warnings.
Diffstat (limited to 'pretyping/patternops.ml')
| -rw-r--r-- | pretyping/patternops.ml | 10 |
1 files changed, 7 insertions, 3 deletions
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml index 4d8c09c50a..41e09004c6 100644 --- a/pretyping/patternops.ml +++ b/pretyping/patternops.ml @@ -59,7 +59,11 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with fixpoint_eq f1 f2 | PCoFix f1, PCoFix f2 -> cofixpoint_eq f1 f2 -| _ -> false +| PProj (p1, t1), PProj (p2, t2) -> + Projection.equal p1 p2 && constr_pattern_eq t1 t2 +| (PRef _ | PVar _ | PEvar _ | PRel _ | PApp _ | PSoApp _ + | PLambda _ | PProd _ | PLetIn _ | PSort _ | PMeta _ + | PIf _ | PCase _ | PFix _ | PCoFix _ | PProj _), _ -> false (** FIXME: fixpoint and cofixpoint should be relativized to pattern *) and pattern_eq (i1, j1, p1) (i2, j2, p2) = @@ -442,8 +446,8 @@ 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) - | r -> err ?loc (Pp.str "Non supported pattern.") - ) + | GPatVar _ | GIf _ | GLetTuple _ | GCases _ | GEvar _ | GRec _ -> + err ?loc (Pp.str "Non supported pattern.")) and pats_of_glob_branches loc metas vars ind brs = let get_arg p = match DAst.get p with |