aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Amélioration message d'erreur quand échec unificationGravatar clrenard2004-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5691 85f007b7-540e-0410-9357-904b9bb8a0f7
* maj annonce depuis la v8beta vers v8Gravatar narboux2004-04-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5690 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5689 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5688 85f007b7-540e-0410-9357-904b9bb8a0f7
* Incorrection exportation XMLGravatar herbelin2004-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5687 85f007b7-540e-0410-9357-904b9bb8a0f7
* Finalement pas de liste des contributions (cela n'avait été fait que pour ↵Gravatar herbelin2004-04-17
| | | | | | la 7.0) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5686 85f007b7-540e-0410-9357-904b9bb8a0f7
* pb facto des Fixpoint + erreur avec -dump-glob et LoadGravatar barras2004-04-17
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5685 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5684 85f007b7-540e-0410-9357-904b9bb8a0f7
* Backtrack user contribsGravatar herbelin2004-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5683 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelles majsGravatar herbelin2004-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5682 85f007b7-540e-0410-9357-904b9bb8a0f7
* TypoGravatar herbelin2004-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5681 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ setupGravatar herbelin2004-04-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5680 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5679 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug réaffichage EXTGravatar herbelin2004-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5678 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2004-04-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5677 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5676 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2004-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5675 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ numéro magiqueGravatar herbelin2004-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5674 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout exemple BrunoGravatar herbelin2004-04-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5673 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5672 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout codingGravatar herbelin2004-04-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5671 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage a la version 1.3 sous GPL des outils okey et configwin de cameleon ↵Gravatar herbelin2004-04-13
| | | | | | en remplacement de la version 1.2 qui etait sous QPL git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5670 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression documentation option raw-comments qui est vraiment trop ad hoc ↵Gravatar herbelin2004-04-13
| | | | | | pour l'export XML des .v git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5669 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction confusion entre la dependance en les termes filtrees dans ↵Gravatar herbelin2004-04-13
| | | | | | l'annotation donnee par l'utilisateur et l'annotation utilisee en interne git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5668 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5667 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5666 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-09
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5665 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5664 85f007b7-540e-0410-9357-904b9bb8a0f7
* Chgt role 2eme argument AList et implantation affichage motifs recursifs de ↵Gravatar herbelin2004-04-08
| | | | | | notations git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5663 85f007b7-540e-0410-9357-904b9bb8a0f7
* Incoherence bytecamlc et camlc si echec a trouver ocamlc.opt avec option ↵Gravatar herbelin2004-04-08
| | | | | | -opt (cd discussion bug #611) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5662 85f007b7-540e-0410-9357-904b9bb8a0f7
* Copyright notice of files in contrib/xml made uniform.Gravatar sacerdot2004-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5661 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5660 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5659 85f007b7-540e-0410-9357-904b9bb8a0f7
* Old file. The new version of this script is no longer distributed withGravatar sacerdot2004-04-07
| | | | | | | Coq (the latest verion can be retrieved from the HELM and MoWGLI pages). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5658 85f007b7-540e-0410-9357-904b9bb8a0f7
* - theoryobject.dtd is the DTD for .theory filesGravatar sacerdot2004-04-07
| | | | | | | - copyright notice inserted in every DTD git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5657 85f007b7-540e-0410-9357-904b9bb8a0f7
* Loic code to pretty-print the generated proof-tree debranched (since itGravatar sacerdot2004-04-07
| | | | | | | | generates not well-formed XML files). An hook is left in xmlcommand.ml to register a pretty-printer function once a fixed implementation is provided. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5656 85f007b7-540e-0410-9357-904b9bb8a0f7
* preparation a la release 8.0Gravatar barras2004-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5655 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2004-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5654 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug #606: mis un message d'erreur plus clairGravatar barras2004-04-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5653 85f007b7-540e-0410-9357-904b9bb8a0f7
* CoRN CProp detection improved: products of "sort" CProp are now recognizedGravatar sacerdot2004-04-07
| | | | | | | (they used to be exported as products of sort Type). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5652 85f007b7-540e-0410-9357-904b9bb8a0f7
* Coqdoc backtrack: HTML special characters are no longer quoted inside # ... #;Gravatar sacerdot2004-04-07
| | | | | | | ^ ... ^ special verbatim code also backtracked. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5651 85f007b7-540e-0410-9357-904b9bb8a0f7
* A few changes backtracked:Gravatar sacerdot2004-04-07
| | | | | | | | | | | | 1. HTML special characters are no longer quoted inside # ... #. 2. ^ ... ^ mode removed. This backtrack makes the HTML generated from CoRN .v files invalid again, since there are '&', '<' and '>' characters inside # ... #. The CoRN stuff agreed to change their .v files accordingly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5650 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5648 85f007b7-540e-0410-9357-904b9bb8a0f7
* 1. In -html mode the generated files are well-formed XML filesGravatar sacerdot2004-04-06
| | | | | | | | | | | | (i.e. the output is no longer HTML but (X)HTML) 2. Added (** ^ ... ^ *) to output verbatim characters that are NOT quoted (whereas (** # ... # *) and all the other similar marks do quote the characters according to the output language quoting conventions). 3. Added ^^ to output a single '^' character git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5647 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fake dependent products in inductive definition types are no longer replacedGravatar sacerdot2004-04-06
| | | | | | | | | | with non dependent products. The main motivation is that inductive definition parameters often occurs as non-dependent products in the product types, but the binder names are still necessary to render the definition in the usual Coq way. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5646 85f007b7-540e-0410-9357-904b9bb8a0f7
* Premier jet annonce finaleGravatar herbelin2004-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5645 85f007b7-540e-0410-9357-904b9bb8a0f7
* Important bug fix: since coqdoc is now quoting XML reserved characters inGravatar sacerdot2004-04-06
| | | | | | | | | HTML tags (i.e. # ... #), strong verbatim tags must be now used (i.e. ^ ... ^). WARNING: it requires the fortcoming commit on coqdoc to work properly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5644 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ V8.0 finaleGravatar herbelin2004-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5643 85f007b7-540e-0410-9357-904b9bb8a0f7
* sumbool et sumor affich avec 'if' si possibleGravatar herbelin2004-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5642 85f007b7-540e-0410-9357-904b9bb8a0f7
* warning dialog when save failsGravatar marche2004-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5641 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 22:59:32 +0000