diff options
| author | Hugo Herbelin | 2019-11-14 07:19:27 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2020-02-22 22:33:40 +0100 |
| commit | 50a39015ea0c86cdb6d368ff7f92ce2091085146 (patch) | |
| tree | 0b4f2fa58277a66f1c74bb757818179c29342f4f | |
| parent | d6467c2fea8a29634ca649850784c95ed5b9d4f4 (diff) | |
Fixing a notation printing bug (missing a @ to reflect absence of imp. args).
When a non-applied reference was matching a notation to the same
reference, implicit arguments were lost.
| -rw-r--r-- | interp/constrextern.ml | 3 | ||||
| -rw-r--r-- | test-suite/output/Notations5.out | 4 | ||||
| -rw-r--r-- | test-suite/output/Notations5.v | 4 |
3 files changed, 5 insertions, 6 deletions
diff --git a/interp/constrextern.ml b/interp/constrextern.ml index 82ba559406..5098b2a00c 100644 --- a/interp/constrextern.ml +++ b/interp/constrextern.ml @@ -1216,7 +1216,7 @@ and extern_notation (custom,scopes as allscopes) vars t rules = (* Note: NApp(NRef f,[]), hence n=0, encodes @f *) (if Int.equal n 0 then f else DAst.make @@ GApp (f,args1)), args2, args2scopes, args2impls - | None when nallargs > 0 -> + | None -> begin match DAst.get f with | GRef (ref,us) -> f, args, argsscopes, argsimpls | _ -> t, [], [], [] @@ -1226,7 +1226,6 @@ and extern_notation (custom,scopes as allscopes) vars t rules = | GRef (ref,us) -> DAst.make @@ GApp (t,[]), [], [], [] | _ -> t, [], [], [] end - | None -> t, [], [], [] | _ -> raise No_match in (* Try matching ... *) let terms,termlists,binders,binderlists = diff --git a/test-suite/output/Notations5.out b/test-suite/output/Notations5.out index 96687ed07f..7afb5ad396 100644 --- a/test-suite/output/Notations5.out +++ b/test-suite/output/Notations5.out @@ -104,9 +104,9 @@ u : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b where ?A : [ |- Type] -u +@u : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b -u +@u : forall (A : Type) (a1 a2 : A) (B : Type) (b : B), a1 = a2 /\ b = b u : forall (a1 a2 : ?A) (B : Type) (b : B), a1 = a2 /\ b = b diff --git a/test-suite/output/Notations5.v b/test-suite/output/Notations5.v index 3c25547aac..92ac4b03ff 100644 --- a/test-suite/output/Notations5.v +++ b/test-suite/output/Notations5.v @@ -145,9 +145,9 @@ Module AppliedTermsPrinting. Check p. (* u *) Check @p. - (* u -- BUG *) + (* @u *) Check @u. - (* u -- BUG *) + (* @u *) Check u. (* u *) Check p 0 0. |