diff options
| -rw-r--r-- | interp/constrextern.ml | 6 | ||||
| -rw-r--r-- | test-suite/output/Notations4.out | 14 | ||||
| -rw-r--r-- | test-suite/output/Notations4.v | 1 |
3 files changed, 13 insertions, 8 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 0396e556cf..a37bac3275 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -453,7 +453,8 @@ let rec extern_cases_pattern_in_scope (custom,scopes as allscopes) vars pat = with No_match -> let loc = pat.CAst.loc in match DAst.get pat with - | PatVar (Name id) when entry_has_ident custom -> CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id))) + | PatVar (Name id) when entry_has_global custom || entry_has_ident custom -> + CAst.make ?loc (CPatAtom (Some (qualid_of_ident ?loc id))) | pat -> match availability_of_entry_coercion custom InConstrEntrySomeLevel with | None -> raise No_match @@ -935,7 +936,8 @@ let rec extern inctx ?impargs scopes vars r = match DAst.get r with | GRef (ref,us) when entry_has_global (fst scopes) -> CAst.make ?loc (extern_ref vars ref us) - | GVar id when entry_has_ident (fst scopes) -> CAst.make ?loc (extern_var ?loc id) + | GVar id when entry_has_global (fst scopes) || entry_has_ident (fst scopes) -> + CAst.make ?loc (extern_var ?loc id) | c -> diff --git a/test-suite/output/Notations4.out b/test-suite/output/Notations4.out index 8948518b3b..f48eaac4c9 100644 --- a/test-suite/output/Notations4.out +++ b/test-suite/output/Notations4.out @@ -16,6 +16,8 @@ Entry constr:myconstr is : option nat [b + c] : nat +fun a : nat => [a + a] + : nat -> nat [1 {f 1}] : Expr fun (x : nat) (y z : Expr) => [1 + y z + {f x}] @@ -83,18 +85,18 @@ fun x : nat => [x] : nat -> nat ∀ x : nat, x = x : Prop -File "stdin", line 225, characters 0-160: +File "stdin", line 226, characters 0-160: Warning: Notation "∀ _ .. _ , _" was already defined with a different format in scope type_scope. [notation-incompatible-format,parsing] ∀x : nat,x = x : Prop -File "stdin", line 238, characters 0-60: +File "stdin", line 239, characters 0-60: Warning: Notation "_ %%% _" was already defined with a different format. [notation-incompatible-format,parsing] -File "stdin", line 242, characters 0-64: +File "stdin", line 243, characters 0-64: Warning: Notation "_ %%% _" was already defined with a different format. [notation-incompatible-format,parsing] -File "stdin", line 247, characters 0-62: +File "stdin", line 248, characters 0-62: Warning: Lonely notation "_ %%%% _" was already defined with a different format. [notation-incompatible-format,parsing] 3 %% 4 @@ -103,9 +105,9 @@ format. [notation-incompatible-format,parsing] : nat 3 %% 4 : nat -File "stdin", line 275, characters 0-61: +File "stdin", line 276, characters 0-61: Warning: The format modifier is irrelevant for only parsing rules. [irrelevant-format-only-parsing,parsing] -File "stdin", line 279, characters 0-63: +File "stdin", line 280, characters 0-63: Warning: The only parsing modifier has no effect in Reserved Notation. [irrelevant-reserved-notation-only-parsing,parsing] diff --git a/test-suite/output/Notations4.v b/test-suite/output/Notations4.v index 08a4480e8a..4d4b37a8b2 100644 --- a/test-suite/output/Notations4.v +++ b/test-suite/output/Notations4.v @@ -27,6 +27,7 @@ Check [ << # 0 >> ]. Axiom c : nat. Notation "x" := x (in custom myconstr at level 0, x global). Check [ b + c ]. +Check fun a => [ a + a ]. End A. |