diff options
| author | Hugo Herbelin | 2017-11-25 17:19:49 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-07-29 02:40:22 +0200 |
| commit | 60daf674df3d11fa2948bbc7c9a928c09f22d099 (patch) | |
| tree | 533584dd6acd3bde940529e8d3a111eca6fcbdef /interp/implicit_quantifiers.ml | |
| parent | 33d86118c7d1bfba31008b410d81c7f45dbdf092 (diff) | |
Adding support for custom entries in notations.
- New command "Declare Custom Entry bar".
- Entries can have levels.
- Printing is done using a notion of coercion between grammar
entries. This typically corresponds to rules of the form
'Notation "[ x ]" := x (x custom myconstr).' but also
'Notation "{ x }" := x (in custom myconstr, x constr).'.
- Rules declaring idents such as 'Notation "x" := x (in custom myconstr, x ident).'
are natively recognized.
- Rules declaring globals such as 'Notation "x" := x (in custom myconstr, x global).'
are natively recognized.
Incidentally merging ETConstr and ETConstrAsBinder.
Noticed in passing that parsing binder as custom was not done as in
constr.
Probably some fine-tuning still to do (priority of notations,
interactions between scopes and entries, ...). To be tested live
further.
Diffstat (limited to 'interp/implicit_quantifiers.ml')
| -rw-r--r-- | interp/implicit_quantifiers.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/implicit_quantifiers.ml b/interp/implicit_quantifiers.ml index 288a0bfe00..4f3037b1fc 100644 --- a/interp/implicit_quantifiers.ml +++ b/interp/implicit_quantifiers.ml @@ -98,7 +98,7 @@ let free_vars_of_constr_expr c ?(bound=Id.Set.empty) l = let rec aux bdvars l c = match CAst.(c.v) with | CRef (qid,_) when qualid_is_ident qid -> found c.CAst.loc (qualid_basename qid) bdvars l - | CNotation ("{ _ : _ | _ }", ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when + | CNotation ((InConstrEntrySomeLevel,"{ _ : _ | _ }"), ({ CAst.v = CRef (qid,_) } :: _, [], [], [])) when qualid_is_ident qid && not (Id.Set.mem (qualid_basename qid) bdvars) -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux (Id.Set.add (qualid_basename qid) bdvars) l c | _ -> Constrexpr_ops.fold_constr_expr_with_binders (fun a l -> Id.Set.add a l) aux bdvars l c |