diff options
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 19 |
1 files changed, 17 insertions, 2 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 20492e38c..326d05cba 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -86,9 +86,11 @@ let rec eq_notation_constr (vars1,vars2 as vars) t1 t2 = match t1, t2 with Miscops.glob_sort_eq s1 s2 | NCast (t1, c1), NCast (t2, c2) -> (eq_notation_constr vars) t1 t2 && cast_type_eq (eq_notation_constr vars) c1 c2 +| NProj (p1, c1), NProj (p2, c2) -> + Projection.equal p1 p2 && eq_notation_constr vars c1 c2 | (NRef _ | NVar _ | NApp _ | NHole _ | NList _ | NLambda _ | NProd _ | NBinderList _ | NLetIn _ | NCases _ | NLetTuple _ | NIf _ - | NRec _ | NSort _ | NCast _), _ -> false + | NRec _ | NSort _ | NCast _ | NProj _), _ -> false (**********************************************************************) (* Re-interpret a notation as a glob_constr, taking care of binders *) @@ -189,6 +191,7 @@ let glob_constr_of_notation_constr_with_binders ?loc g f e nc = | NSort x -> GSort x | NHole (x, naming, arg) -> GHole (x, naming, arg) | NRef x -> GRef (x,None) + | NProj (p,c) -> GProj (p, f e c) let glob_constr_of_notation_constr ?loc x = let rec aux () x = @@ -383,6 +386,7 @@ let notation_constr_and_vars_of_glob_constr a = if arg != None then has_ltac := true; NHole (w, naming, arg) | GRef (r,_) -> NRef r + | GProj (p, c) -> NProj (p, aux c) | GEvar _ | GPatVar _ -> user_err Pp.(str "Existential variables not allowed in notations.") ) x @@ -576,6 +580,14 @@ let rec subst_notation_constr subst bound raw = let k' = Miscops.smartmap_cast_type (subst_notation_constr subst bound) k in if r1' == r1 && k' == k then raw else NCast(r1',k') + | NProj (p, c) -> + let kn = Projection.constant p in + let b = Projection.unfolded p in + let kn' = subst_constant subst kn in + let c' = subst_notation_constr subst bound c in + if kn' == kn && c' == c then raw else NProj(Projection.make kn' b, c') + + let subst_interpretation subst (metas,pat) = let bound = List.fold_left (fun accu (id, _) -> Id.Set.add id accu) Id.Set.empty metas in (metas,subst_notation_constr subst bound pat) @@ -1167,9 +1179,12 @@ let rec match_ inner u alp metas sigma a1 a2 = match_names metas (alp,sigma) (Name id') na in match_in u alp metas sigma (mkGApp a1 (DAst.make @@ GVar id')) b2 + | GProj(p1, t1), NProj(p2, t2) when Projection.equal p1 p2 -> + match_in u alp metas sigma t1 t2 + | (GRef _ | GVar _ | GEvar _ | GPatVar _ | GApp _ | GLambda _ | GProd _ | GLetIn _ | GCases _ | GLetTuple _ | GIf _ | GRec _ | GSort _ | GHole _ - | GCast _), _ -> raise No_match + | GCast _ | GProj _ ), _ -> raise No_match and match_in u = match_ true u |