blob: ee84cb94e97cddab410adfd0da3cbb66e09957fd (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
Lemma a : True.
Proof.
assert True as H.
abstract (trivial) using exported_seff.
exact H.
Fail Qed export a_subproof.
Qed export exported_seff.
Check ( exported_seff : True ).
Lemma b : True.
Proof.
assert True as H.
abstract (trivial) using exported_seff2.
exact H.
Qed.
Fail Check ( exported_seff2 : True ).
|
