diff options
| author | Hugo Herbelin | 2020-10-24 14:45:57 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-20 19:41:20 +0100 |
| commit | 93654a0ba50f26f90f84e98b33ec13caa92d1799 (patch) | |
| tree | 9ee57efbb938eeadf37e0ea80ba73bd7cb0a1722 /interp/constrintern.ml | |
| parent | 23924afa0e4d7ed9ca58fbf5f69dc57685d593fa (diff) | |
Enforcing when a binding variable has no explicit type in constr_notation.
This avoids relying on fragile invariants.
Diffstat (limited to 'interp/constrintern.ml')
| -rw-r--r-- | interp/constrintern.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/interp/constrintern.ml b/interp/constrintern.ml index 1a922eb9a4..8bd77abc4a 100644 --- a/interp/constrintern.ml +++ b/interp/constrintern.ml @@ -928,10 +928,10 @@ let instantiate_notation_constr loc intern intern_pat ntnvars subst infos c = aux (terms,None,Some (l,terminator,iter)) subinfos (NVar ldots_var) with Not_found -> anomaly (Pp.str "Inconsistent substitution of recursive notation.")) - | NProd (Name id, NHole _, c') when option_mem_assoc id binderopt -> + | NProd (Name id, None, c') when option_mem_assoc id binderopt -> let binder = snd (Option.get binderopt) in expand_binders ?loc mkGProd [binder] (aux subst' (renaming,env) c') - | NLambda (Name id,NHole _,c') when option_mem_assoc id binderopt -> + | NLambda (Name id, None, c') when option_mem_assoc id binderopt -> let binder = snd (Option.get binderopt) in expand_binders ?loc mkGLambda [binder] (aux subst' (renaming,env) c') | t -> |