diff options
| author | Enrico Tassi | 2015-06-29 21:30:19 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2015-06-29 22:16:07 +0200 |
| commit | 2defd4c15467736b73f69adb501e3a4fe2111ce5 (patch) | |
| tree | 6a73e7280956a90e6eb8a588f64a208a3624cd5c /pretyping/termops.mli | |
| parent | 799f27ae19d6d2d16ade15bbdab83bd9acb0035f (diff) | |
Assumptions: more informative print for False axiom (Close: #4054)
When an axiom of an empty type is matched in order to inhabit
a type, do print that type (as if each use of that axiom was a
distinct foo_subproof).
E.g.
Lemma w : True.
Proof. case demon. Qed.
Lemma x y : y = 0 /\ True /\ forall w, w = y.
Proof. split. case demon. split; [ exact w | case demon ]. Qed.
Print Assumptions x.
Prints:
Axioms:
demon : False
used in x to prove: forall w : nat, w = y
used in w to prove: True
used in x to prove: y = 0
Diffstat (limited to 'pretyping/termops.mli')
| -rw-r--r-- | pretyping/termops.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/pretyping/termops.mli b/pretyping/termops.mli index 2552c67e61..4581e23100 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -84,6 +84,10 @@ val map_constr_with_full_binders : val fold_constr_with_binders : ('a -> 'a) -> ('a -> 'b -> constr -> 'b) -> 'a -> 'b -> constr -> 'b +val fold_constr_with_full_binders : + (rel_declaration -> 'a -> 'a) -> ('a -> 'b -> constr -> 'b) -> + 'a -> 'b -> constr -> 'b + val iter_constr_with_full_binders : (rel_declaration -> 'a -> 'a) -> ('a -> constr -> unit) -> 'a -> constr -> unit |