aboutsummaryrefslogtreecommitdiffhomepage
path: root/COMPATIBILITY
Commit message (Collapse)AuthorAge
* [vernac] Remove `Qed exporting` syntax.Gravatar Emilio Jesus Gallego Arias2017-09-29
| | | | | | | We don't gain anything from the kernel yet as transparent constants _do_ require the `side_eff` exporting machinery. Next step, understand why.
* A fix for #5390 (a useful error on used introduction names was masked).Gravatar Hugo Herbelin2017-05-17
| | | | | | | | | | | | | | With the "apply in" introduction pattern, and the backtrack possibly done in "apply" over the components of conjunctions (descend_in_conjunctions), the reasons for failing might have different sources. We give priority to the detection of used names over other (unification) errors so that an error there is not masked in the backtracking made by descend_in_conjunctions. Of course, the question of what best unification error to give in the presence of backtracking is still open.
* Being more informative about the change of behavior of "subst".Gravatar Hugo Herbelin2016-09-29
|
* Update CHANGES and COMPATIBILITYGravatar Matthieu Sozeau2016-06-27
|
* Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2016-05-20
|\
| * More hints on how to fix compatibility issues.Gravatar Hugo Herbelin2016-05-14
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-03-23
|\|
| * Qed export -> Qed exportingGravatar Enrico Tassi2015-03-22
| |
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-15
|\|
| * typoGravatar Enrico Tassi2015-02-14
| |
| * Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorGravatar Enrico Tassi2015-02-14
| | | | | | | | Of course such proofs cannot be processed asynchronously
* | Merge branch 'v8.5'Gravatar Pierre-Marie Pédrot2015-02-13
|\|
| * COMPATIBILITY: add note about the change of behavior of Instance foo :=Gravatar Matthieu Sozeau2015-02-12
| | | | | | | | {| |}. Add test-suite files for closed bugs.
* | Added stuff about -I -Q -R in COMPATIBILTY.Gravatar Pierre Courtieu2015-01-15
| |
* | Mention CHANGES file in COMPATIBILITY.Gravatar Maxime Dénès2015-01-15
| |
| * Mention CHANGES file in COMPATIBILITY.Gravatar Maxime Dénès2015-01-15
|/
* Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameGravatar Matthieu Sozeau2014-10-11
| | | | | | | for the record binder of classes. This name is no longer generated in the kernel but part of the declaration. Also cleanup the interface to recognize primitive records based on an option type instead of a dynamic check of the length of an array.
* Give the same argument name for the record binder of type classGravatar Matthieu Sozeau2014-10-10
| | | | | projections and regular records. Easily fixable backwards incompatibility.
* Updating CHANGES w.r.t. opacity in type inference + layout of file.Gravatar Hugo Herbelin2014-06-28
|
* Add some compatibility notes on the changes to [change] and unification in ↵Gravatar Matthieu Sozeau2014-06-23
| | | | general.
* Some extra INCOMPATIBILITIES since 8.4.Gravatar herbelin2012-08-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15732 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cleaning CHANGES consistently with v8.4. Documenting COMPATIBILITY.Gravatar herbelin2012-08-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15711 85f007b7-540e-0410-9357-904b9bb8a0f7
* Credits for 8.4 + resetting COMPATIBILITY file.Gravatar herbelin2011-12-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14846 85f007b7-540e-0410-9357-904b9bb8a0f7
* Removed information in COMPATIBILITY that were intended before all forGravatar herbelin2010-07-30
| | | | | | developers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13364 85f007b7-540e-0410-9357-904b9bb8a0f7
* Miscellaneous small updates:Gravatar herbelin2010-07-01
| | | | | | | - removed call to obsolete ppmsid printer in 8.3 - updated COMPATIBILITY file git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13229 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improving compatibility between 8.2 and 8.3Gravatar herbelin2010-04-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12904 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ diversesGravatar herbelin2008-06-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11102 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Patch sur "intros until 0"Gravatar herbelin2008-06-08
| | | | | | | | | - MAJ CHANGES et COMPATIBILITY - Réservation de || et && dans Notations.v - code mort et MAJ suite commit 11072 (tactics.ml et changes.txt) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11073 85f007b7-540e-0410-9357-904b9bb8a0f7
* Quelques infos pour la portabilité 8.1 --> 8.2Gravatar notin2008-06-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix setoid_rewrite documentation examples.Gravatar msozeau2008-06-03
| | | | | | | | | | Debug handling of identifiers in coqdoc (should work with modules and sections) and add missing macros. Move theories/Program to THEORIESVO to put the files in the standard library documentation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11046 85f007b7-540e-0410-9357-904b9bb8a0f7
* - Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"Gravatar herbelin2008-05-30
| | | | | | | | | | n'étaient pas gérés, merci à Julien). - Correction pb blocage CoqIDE quand le browser n'est pas déja lancé (utilisation pour cela de Sys.command au lieu de Unix.open_process_full). - MAJ CHANGES et COMPATIBILITY. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11022 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2006-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9254 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2006-07-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9022 85f007b7-540e-0410-9357-904b9bb8a0f7
* Typo in case of reference to dev/doc/changes.txtGravatar lmamane2006-06-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8958 85f007b7-540e-0410-9357-904b9bb8a0f7
* A list of incompatibilitiesGravatar herbelin2006-06-14
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8955 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-13 18:42:00 +0000