diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2017-08-13 20:05:03 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2018-02-20 10:03:04 +0100 |
| commit | d4c2ed95fcfd64cdcc10e51e40be739d9f1c4a74 (patch) | |
| tree | 4843bf72c79905f811d6f3f5ac4cdd4d81943e65 /interp/constrintern.ml | |
| parent | 7c10b4020e061fb14e01cb3abc92bb5265aa65b9 (diff) | |
Allows recursive patterns for binders to be associative on the left.
This makes treatment of recursive binders closer to the one of
recursive terms. It is unclear whether there are interesting notations
liable to use this, but this shall make easier mixing recursive
binders and recursive terms as in next commits.
Example of (artificial) notation that this commit supports:
Notation "! x .. y # A #" :=
(.. (A,(forall x, True)) ..,(forall y, True))
(at level 200, x binder).
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 3c8643ee3..bedf932b0 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -663,12 +663,13 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = Some (Genintern.generic_substitute_notation bindings arg) in DAst.make ?loc @@ GHole (knd, naming, arg) - | NBinderList (x,y,iter,terminator) -> + | NBinderList (x,y,iter,terminator,lassoc) -> (try (* All elements of the list are in scopes (scopt,subscopes) *) let (bl,(scopt,subscopes)) = Id.Map.find x binders in (* We flatten binders so that we can interpret them at substitution time *) let bl = flatten_binders bl in + let bl = if lassoc then List.rev bl else bl in (* We isolate let-ins which do not contribute to the repeated pattern *) let l = List.map (function | CLocalDef (na,c,t) -> AddLetIn (na,c,t) | binder -> AddPreBinderIter (y,binder)) bl in |