diff options
| author | Hugo Herbelin | 2017-08-14 01:27:04 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2018-02-20 10:03:04 +0100 |
| commit | a18e87f6a929ce296f8c277b310e286151e06293 (patch) | |
| tree | 703657d008ea6a21e7e230b3b27a9ce2618e0f65 /interp/constrintern.ml | |
| parent | d4c2ed95fcfd64cdcc10e51e40be739d9f1c4a74 (diff) | |
Allowing variables used in recursive notation to occur several times in pattern.
This allows for instance to support recursive notations of the form:
Notation "! x .. y # A #" :=
(((forall x, x=x),(forall x, x=0)), .. (((forall y, y=y),(forall y, y=0)), A) ..)
(at level 200, x binder).
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 10 |
1 files changed, 9 insertions, 1 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index bedf932b03..7411c7e357 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -697,7 +697,7 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = | t -> glob_constr_of_notation_constr_with_binders ?loc (traverse_binder subst avoid) (aux subst') subinfos t - and subst_var (terms, _binderopt, _terminopt) (renaming, env) id = + and subst_var (terms, binderopt, _terminopt) (renaming, env) id = (* subst remembers the delimiters stack in the interpretation *) (* of the notations *) try @@ -705,6 +705,14 @@ let instantiate_notation_constr loc intern ntnvars subst infos c = intern {env with tmp_scope = scopt; scopes = subscopes @ env.scopes} a with Not_found -> + try + match binderopt with + | Some (x,binder) when Id.equal x id -> + let terms = terms_of_binders [binder] in + assert (List.length terms = 1); + intern env (List.hd terms) + | _ -> raise Not_found + with Not_found -> DAst.make ?loc ( try GVar (Id.Map.find id renaming) |