diff options
| author | coqbot-app[bot] | 2020-08-31 12:09:18 +0000 |
|---|---|---|
| committer | GitHub | 2020-08-31 12:09:18 +0000 |
| commit | daca83946ed5a001f2461fefa787a80f7dcdea01 (patch) | |
| tree | 0a746f4f5496290ca18c5d92d57cb7d3a9c89065 /test-suite/output/InitSyntax.out | |
| parent | b4ff2af4f43a2e0ba40c7f8a6260da1c75859045 (diff) | |
| parent | 8262041215c9bc3d13e768b1c422b52005083e85 (diff) | |
Merge PR #12875: Further extensions of About wrt Arguments and renaming
Reviewed-by: SkySkimmer
Ack-by: herbelin
Diffstat (limited to 'test-suite/output/InitSyntax.out')
| -rw-r--r-- | test-suite/output/InitSyntax.out | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/test-suite/output/InitSyntax.out b/test-suite/output/InitSyntax.out index da255e86cd..02e58775b5 100644 --- a/test-suite/output/InitSyntax.out +++ b/test-suite/output/InitSyntax.out @@ -2,7 +2,7 @@ Inductive sig2 (A : Type) (P Q : A -> Prop) : Type := exist2 : forall x : A, P x -> Q x -> {x : A | P x & Q x} Arguments sig2 [A]%type_scope (_ _)%type_scope -Arguments exist2 [A]%type_scope (_ _)%function_scope +Arguments exist2 [A]%type_scope (_ _)%function_scope _ _ _ exists x : nat, x = x : Prop fun b : bool => if b then b else b |