diff options
| author | Hugo Herbelin | 2017-08-12 09:15:40 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:06 +0100 |
| commit | edd0d22429354a5f2c703a8c7bd1f775e2f97d9e (patch) | |
| tree | 865fd16d40f5641cac233f951f951a9a4502159f /interp/constrintern.mli | |
| parent | 398358618bb3eabfe822b79c669703c1c33b67e6 (diff) | |
Adding support for parsing subterms of a notation as "pattern".
This allows in particular to define notations with 'pat style binders.
E.g.:
A non-trivial change in this commit is storing binders and patterns
separately from terms.
This is not strictly necessary but has some advantages.
However, it is relatively common to have binders also used as terms,
or binders parsed as terms. Thus, it is already relatively common to
embed binders into terms (see e.g. notation for ETA in output test
Notations3.v) or to coerce terms to idents (see e.g. the notation for
{x|P} where x is parsed as a constr).
So, it is as simple to always store idents (and eventually patterns)
as terms.
Diffstat (limited to 'interp/constrintern.mli')
| -rw-r--r-- | interp/constrintern.mli | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/interp/constrintern.mli b/interp/constrintern.mli index 87b587b71c..f09b17a49f 100644 --- a/interp/constrintern.mli +++ b/interp/constrintern.mli @@ -87,7 +87,7 @@ val intern_gen : typing_constraint -> env -> constr_expr -> glob_constr val intern_pattern : env -> cases_pattern_expr -> - Id.t list * (Id.t Id.Map.t * cases_pattern) list + Id.t Loc.located list * (Id.t Id.Map.t * cases_pattern) list val intern_context : bool -> env -> internalization_env -> local_binder_expr list -> internalization_env * glob_decl list @@ -184,8 +184,7 @@ val global_reference_in_absolute_module : DirPath.t -> Id.t -> Globnames.global_ guaranteed to have the same domain as the input one. *) val interp_notation_constr : env -> ?impls:internalization_env -> notation_interp_env -> constr_expr -> - (bool * subscopes * notation_var_internalization_type) Id.Map.t * - notation_constr * reversibility_status + (bool * subscopes) Id.Map.t * notation_constr * reversibility_status (** Globalization options *) val parsing_explicit : bool ref |