blob: b3e41ab1fbc43d9d05cb5fd7d022764b70b47ef6 (
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 exporting a_subproof.
Qed exporting 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 ).
|
