| Commit message (Collapse) | Author | Age | |
|---|---|---|---|
| * | Fixing tauto "special" behavior on singleton types w/ 2 parameters (bug #2680). |  herbelin | 2012-04-15 |
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | - tauto/intuition now works uniformly on and, prod, or, sum, False, Empty_set, unit, True (and isomorphic copies of them), iff, ->, and on all inhabited singleton types with a no-arguments constructor such as "eq t t" (even though the last case goes out of propositional logic: this features is so often used that it is difficult to come back on it). - New dtauto and dintuition works on all inductive types with one constructors and no real arguments (for instance, they work on records such as "Equivalence"), in addition to -> and eq-like types. - Moreover, both of them no longer unfold inner negations (this is a souce of incompatibility for intuition and evaluation of the level of incompatibility on contribs still needs to be done). Incidentally, and amazingly, fixing bug #2680 made that constants InfA_compat and InfA_eqA in SetoidList.v lost one argument: old tauto had indeed destructed a section hypothesis "@StrictOrder A ltA@ thinking it was a conjunction, making this section hypothesis artificially necessary while it was not. Renouncing to the unfolding of inner negations made auto/eauto sometimes succeeding more, sometimes succeeding less. There is by the way a (standard) problem with not in auto/eauto: even when given as an "unfold hint", it works only in goals, not in hypotheses, so that auto is not able to solve something like "forall P, (forall x, ~ P x) -> P 0 -> False". Should we automatically add a lemma of type "HYPS -> A -> False" in the hint database everytime a lemma ""HYPS -> ~A" is declared (and "unfold not" is a hint), and similarly for all unfold hints? At this occasion, also re-did some proofs of Znumtheory. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15180 85f007b7-540e-0410-9357-904b9bb8a0f7 | ||
| * | Revert "Tentative to fix bug #2628 by not letting intuition break records. ↵ |  msozeau | 2012-01-31 |
| | | | | | | | | | | Might be too much of a backwards-incompatible change" Indeed it is breaking too many scripts. This reverts commit 47e9afaaa4c08aca97d4f4b5a89cb40da76bd850. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14956 85f007b7-540e-0410-9357-904b9bb8a0f7 | ||
| * | Tentative to fix bug #2628 by not letting intuition break records. Might be ↵ | msozeau | 2012-01-28 |
| | | | | | | | too much of a backwards-incompatible change git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14949 85f007b7-540e-0410-9357-904b9bb8a0f7 | ||
| * | - Add modulo_delta_types flag for unification to allow full | msozeau | 2011-03-13 |
| | | | | | | | | | | | | | | | | | conversion when checking types of instanciations while having restricted delta reduction for unification itself. This makes auto/eauto... backward compatible. - Change semantics of [Instance foo : C a.] to _not_ search for an instance of [C a] automatically and potentially slow down interaction, except for trivial classes with no fields. Use [C a := _.] or [C a := {}] to search for an instance of the class or for every field. - Correct treatment of transparency information for classes declared in sections. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13908 85f007b7-540e-0410-9357-904b9bb8a0f7 | ||
| * | Nicer names: DecidableType2* --> Equalities*, OrderedType2* --> Orders* |  letouzey | 2010-01-07 |
| Old stuff DecidableType.v and OrderedType.v stay there and keep their names for the moment, for compatibility. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12641 85f007b7-540e-0410-9357-904b9bb8a0f7 | |||
 |
index : coq | |
| the Coq proof assistant |
| aboutsummaryrefslogtreecommitdiffhomepage |