| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fix #3948 Anomaly: unknown constant in Print Assumptions |  Maxime Dénès | 2015-09-20 |
| | | | | | | Substitution on bound modules was incorrectly extended without sequential composition. | ||
| * | Fixing bug #4269: [Print Assumptions] lies about which axioms a term depends on. |  Pierre-Marie Pédrot | 2015-09-15 |
| | | | | | | This was because the traversal algorithm used canonical names instead of user names, confusing which term was defined and which term was an axiom. | ||
| * | Fix loop in assumptions (Close: #4275) |  Enrico Tassi | 2015-07-02 |
| | | |||
| * | Assumptions: more informative print for False axiom (Close: #4054) | Enrico Tassi | 2015-06-29 |
| 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 | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |