diff options
| author |  Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-27 18:29:39 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias <e+git@x80.org> | 2018-06-27 18:29:39 +0200 |
| commit | c33988dafcad14f9f0c10a287d2cfb2790e253c4 (patch) | |
| tree | eba36b138067491f49fd12656df98d73ac8e7742 /interp | |
| parent | 04e0f9fde8789a28b66f24000ac8c831ff0815af (diff) | |
| parent | 8d9b66bed22364f513771e9b1fa3df14a3dab866 (diff) | |
Merge PR #7924: Ad hoc fix for #5696, #7903 (ltac subterms and open subterms in notations).
Diffstat (limited to 'interp')
| -rw-r--r-- | interp/constrintern.ml | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 4e217b2cd..18d6c1a5b 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -710,10 +710,12 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = let arg = match arg with | None -> None | Some arg -> - let mk_env (c, (tmp_scope, subscopes)) = + let mk_env id (c, (tmp_scope, subscopes)) map = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in - let gc = intern nenv c in - (gc, Some c) + try + let gc = intern nenv c in + Id.Map.add id (gc, Some c) map + with GlobalizationError _ -> map in let mk_env' (c, (onlyident,(tmp_scope,subscopes))) = let nenv = {env with tmp_scope; scopes = subscopes @ env.scopes} in @@ -725,7 +727,7 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = | [pat] -> (glob_constr_of_cases_pattern pat, None) | _ -> error_cannot_coerce_disjunctive_pattern_term ?loc:c.loc () in - let terms = Id.Map.map mk_env terms in + let terms = Id.Map.fold mk_env terms Id.Map.empty in let binders = Id.Map.map mk_env' binders in let bindings = Id.Map.fold Id.Map.add terms binders in Some (Genintern.generic_substitute_notation bindings arg) |