From 97fefe1fcca363a1317e066e7f4b99b9c1e9987b Mon Sep 17 00:00:00 2001 From: Stephane Glondu Date: Thu, 12 Jan 2012 16:02:20 +0100 Subject: Imported Upstream version 8.4~beta --- test-suite/output/Arguments_renaming.v | 54 ++++++++++++++++++++++++++++++++++ 1 file changed, 54 insertions(+) create mode 100644 test-suite/output/Arguments_renaming.v (limited to 'test-suite/output/Arguments_renaming.v') 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. + + -- cgit v1.2.3