diff options
| author | Hugo Herbelin | 2020-04-13 20:01:29 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2020-11-05 19:09:07 +0100 |
| commit | cb105b62f597b2a51fad743547647e4885d6365a (patch) | |
| tree | 3bafd03e6e9413014a4bd5af39dc028fb65c8a9d /interp/notation_ops.ml | |
| parent | d276a494d29ea69c6a60b16da5dddb9d39f287ca (diff) | |
Notations: Giving a consistent role to global references occurring patterns.
Currently, global references in patterns used also as terms were
accepted for parsing but not for printing.
We accept section variables for both parsing and printing. We reject
constant and inductive types for both parsing and printing.
Among other, this also fixes a hole in interpreting variables used
both patterns and terms: the term part was not interpreted.
Diffstat (limited to 'interp/notation_ops.ml')
| -rw-r--r-- | interp/notation_ops.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml index 24b5dfce29..34e94d1597 100644 --- a/interp/notation_ops.ml +++ b/interp/notation_ops.ml @@ -941,7 +941,7 @@ let bind_term_as_binding_env alp (terms,termlists,binders,binderlists as sigma) try (* If already bound to a term, unify the binder and the term *) match DAst.get (Id.List.assoc var terms) with - | GVar id' -> + | GVar id' | GRef (GlobRef.VarRef id',None) -> (if not (Id.equal id id') then (fst alp,(id,id')::snd alp) else alp), sigma | t -> |