diff options
author | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-21 17:03:54 +0000 |
---|---|---|
committer | gareuselesinge <gareuselesinge@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-11-21 17:03:54 +0000 |
commit | 39fd2b160dbbd6411dd05f52984f198338de300a (patch) | |
tree | fba087dc2d603fc969c8b6193662f01ffcc9f08f /test-suite/output/Arguments_renaming.v | |
parent | ed06a90f16fcf7d45672bbddf42efe4cc0efd4d4 (diff) |
Renamig support added to "Arguments"
Example:
Arguments eq_refl {B y}, [B] y.
Check (eq_refl (B := nat)).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14719 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'test-suite/output/Arguments_renaming.v')
-rw-r--r-- | test-suite/output/Arguments_renaming.v | 48 |
1 files changed, 48 insertions, 0 deletions
diff --git a/test-suite/output/Arguments_renaming.v b/test-suite/output/Arguments_renaming.v new file mode 100644 index 000000000..7cbb6801e --- /dev/null +++ b/test-suite/output/Arguments_renaming.v @@ -0,0 +1,48 @@ +Arguments eq_refl {B y}, [B] y. +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 _. +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. + +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. |