diff options
author | Enrico Tassi <gareuselesinge@debian.org> | 2016-01-26 16:56:33 +0100 |
---|---|---|
committer | Enrico Tassi <gareuselesinge@debian.org> | 2016-01-26 16:56:33 +0100 |
commit | 164c6861860e6b52818c031f901ffeff91fca16a (patch) | |
tree | 4f91d20c890c25915e7b28226c663b94a8cfb0d3 /test-suite/success/polymorphism.v | |
parent | 91dbeab8eef959c3f64960909ca69d4e68c8198d (diff) |
Imported Upstream version 8.5upstream/8.5
Diffstat (limited to 'test-suite/success/polymorphism.v')
-rw-r--r-- | test-suite/success/polymorphism.v | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/test-suite/success/polymorphism.v b/test-suite/success/polymorphism.v index d6bbfe29..878875bd 100644 --- a/test-suite/success/polymorphism.v +++ b/test-suite/success/polymorphism.v @@ -242,7 +242,7 @@ Fail Check (Prop : Set). Fail Check (Set : Set). Check (Set : Type). Check (Prop : Type). -Definition setType := $(let t := type of Set in exact t)$. +Definition setType := ltac:(let t := type of Set in exact t). Definition foo (A : Prop) := A. @@ -303,7 +303,7 @@ Set Printing Universes. Axiom admit : forall A, A. Record R := {O : Type}. -Definition RL (x : R@{i}) : $(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) )$ := {|O := @O x|}. +Definition RL (x : R@{i}) : ltac:(let u := constr:(Type@{i}:Type@{j}) in exact (R@{j}) ) := {|O := @O x|}. Definition RLRL : forall x : R, RL x = RL (RL x) := fun x => eq_refl. Definition RLRL' : forall x : R, RL x = RL (RL x). intros. apply eq_refl. |