diff options
author | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2013-05-08 18:03:54 +0200 |
commit | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (patch) | |
tree | 09dafc3e5c7361d3a28e93677eadd2b7237d4f9f /test-suite/output/Arguments_renaming.v | |
parent | 6e34b272d789455a9be589e27ad3a998cf25496b (diff) | |
parent | 499a11a45b5711d4eaabe84a80f0ad3ae539d500 (diff) |
Merge branch 'experimental/upstream' into upstream
Diffstat (limited to 'test-suite/output/Arguments_renaming.v')
-rw-r--r-- | test-suite/output/Arguments_renaming.v | 54 |
1 files changed, 54 insertions, 0 deletions
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v new file mode 100644 index 00000000..b133e733 --- /dev/null +++ b/test-suite/output/Arguments_renaming.v @@ -0,0 +1,54 @@ +Fail Arguments eq_refl {B y}, [B] y. +Fail Arguments identity T _ _. +Arguments eq_refl A x. +Arguments eq_refl {B y}, [B] y : rename. + +Check @eq_refl. +Check (eq_refl (B := nat)). +Print eq_refl. +About eq_refl. + +Goal 3 = 3. +apply @eq_refl with (B := nat). +Undo. +apply @eq_refl with (y := 3). +Undo. +pose (y := nat). +apply (@eq_refl y) with (y0 := 3). +Qed. + +Section Test1. + +Variable A : Type. + +Inductive myEq B (x : A) : A -> Prop := myrefl : B -> myEq B x x. + +Global Arguments myrefl {C} x _ : rename. +Print myrefl. +About myrefl. + +Fixpoint myplus T (t : T) (n m : nat) {struct n} := + match n with O => m | S n' => S (myplus T t n' m) end. + +Global Arguments myplus {Z} !t !n m : rename. + +Print myplus. +About myplus. +Check @myplus. + +End Test1. +Print myrefl. +About myrefl. +Check myrefl. + +Print myplus. +About myplus. +Check @myplus. + +Fail Arguments eq_refl {F g}, [H] k. +Fail Arguments eq_refl {F}, [F]. +Fail Arguments eq_refl {F F}, [F] F. +Fail Arguments eq {F} x [z]. +Fail Arguments eq {F} x z y. + + |