diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-04 16:33:30 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-04-04 17:26:10 +0200 |
commit | 4bce91623c2857f843129e927fdadb30a9c87a7e (patch) | |
tree | 16fb276aabd4966fa210b511fb34bae7612188d7 /test-suite/success/abstract_chain.v | |
parent | ba70b9c2ac6d705d4f55d516a7631694cdc9f94e (diff) |
Adding tests for chained abstract tactics.
Diffstat (limited to 'test-suite/success/abstract_chain.v')
-rw-r--r-- | test-suite/success/abstract_chain.v | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/test-suite/success/abstract_chain.v b/test-suite/success/abstract_chain.v new file mode 100644 index 000000000..0ff61e87f --- /dev/null +++ b/test-suite/success/abstract_chain.v @@ -0,0 +1,43 @@ +Lemma foo1 : nat -> True. +Proof. +intros _. +assert (H : True -> True). +{ abstract (exact (fun x => x)) using bar. } +assert (H' : True). +{ abstract (exact (bar I)) using qux. } +exact H'. +Qed. + +Lemma foo2 : True. +Proof. +assert (H : True -> True). +{ abstract (exact (fun x => x)) using bar. } +assert (H' : True). +{ abstract (exact (bar I)) using qux. } +assert (H'' : True). +{ abstract (exact (bar qux)) using quz. } +exact H''. +Qed. + +Set Universe Polymorphism. + +Lemma foo3 : nat -> True. +Proof. +intros _. +assert (H : True -> True). +{ abstract (exact (fun x => x)) using bar. } +assert (H' : True). +{ abstract (exact (bar I)) using qux. } +exact H'. +Qed. + +Lemma foo4 : True. +Proof. +assert (H : True -> True). +{ abstract (exact (fun x => x)) using bar. } +assert (H' : True). +{ abstract (exact (bar I)) using qux. } +assert (H'' : True). +{ abstract (exact (bar qux)) using quz. } +exact H''. +Qed. |