aboutsummaryrefslogtreecommitdiff
path: root/COMPATIBILITY
AgeCommit message (Collapse)Author
2018-01-22Archive COMPATIBILITY.Théo Zimmermann
2018-01-22Move the mention of the removal of Qed exporting at the right place.Théo Zimmermann
2017-09-29[vernac] Remove `Qed exporting` syntax.Emilio Jesus Gallego Arias
We don't gain anything from the kernel yet as transparent constants _do_ require the `side_eff` exporting machinery. Next step, understand why.
2017-05-17A fix for #5390 (a useful error on used introduction names was masked).Hugo Herbelin
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.
2016-09-29Being more informative about the change of behavior of "subst".Hugo Herbelin
2016-06-27Update CHANGES and COMPATIBILITYMatthieu Sozeau
2016-05-20Merge branch 'v8.5'Pierre-Marie Pédrot
2016-05-14More hints on how to fix compatibility issues.Hugo Herbelin
2015-03-23Merge branch 'v8.5'Pierre-Marie Pédrot
2015-03-22Qed export -> Qed exportingEnrico Tassi
2015-02-15Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-14typoEnrico Tassi
2015-02-14Abstract: "Qed export ident, .., ident" to preserve v8.4 behaviorEnrico Tassi
Of course such proofs cannot be processed asynchronously
2015-02-13Merge branch 'v8.5'Pierre-Marie Pédrot
2015-02-12COMPATIBILITY: add note about the change of behavior of Instance foo :=Matthieu Sozeau
{| |}. Add test-suite files for closed bugs.
2015-01-15Added stuff about -I -Q -R in COMPATIBILTY.Pierre Courtieu
2015-01-15Mention CHANGES file in COMPATIBILITY.Maxime Dénès
2015-01-15Mention CHANGES file in COMPATIBILITY.Maxime Dénès
2014-10-11Revert d0cd27e209be08ee51a2d609157367f053438a10: giving a different nameMatthieu Sozeau
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.
2014-10-10Give the same argument name for the record binder of type classMatthieu Sozeau
projections and regular records. Easily fixable backwards incompatibility.
2014-06-28Updating CHANGES w.r.t. opacity in type inference + layout of file.Hugo Herbelin
2014-06-23Add some compatibility notes on the changes to [change] and unification in ↵Matthieu Sozeau
general.
2012-08-11Some extra INCOMPATIBILITIES since 8.4.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15732 85f007b7-540e-0410-9357-904b9bb8a0f7
2012-08-08Cleaning CHANGES consistently with v8.4. Documenting COMPATIBILITY.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15711 85f007b7-540e-0410-9357-904b9bb8a0f7
2011-12-22Credits for 8.4 + resetting COMPATIBILITY file.herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14846 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-30Removed information in COMPATIBILITY that were intended before all forherbelin
developers. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13364 85f007b7-540e-0410-9357-904b9bb8a0f7
2010-07-01Miscellaneous small updates:herbelin
- 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
2010-04-05Improving compatibility between 8.2 and 8.3herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12904 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-11MAJ diversesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11102 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-08- Patch sur "intros until 0"herbelin
- 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
2008-06-05Quelques infos pour la portabilité 8.1 --> 8.2notin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11057 85f007b7-540e-0410-9357-904b9bb8a0f7
2008-06-03Fix setoid_rewrite documentation examples.msozeau
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
2008-05-30- Correction d'un nouveau bug de undo de CoqIDE ("Admitted" et "Proof t"herbelin
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
2006-10-20MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9254 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-07-05MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9022 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-15Typo in case of reference to dev/doc/changes.txtlmamane
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8958 85f007b7-540e-0410-9357-904b9bb8a0f7
2006-06-14A list of incompatibilitiesherbelin
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.25.1) at 2026-01-31 20:19:13 +0000