aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* 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
* Bug sur commit 1.44 dans find_constructor (Not_Found pas rattrape)Gravatar herbelin2004-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5640 85f007b7-540e-0410-9357-904b9bb8a0f7
* echappement de <, > et & en HTMLGravatar filliatr2004-04-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5639 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5638 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déclaration des record au chargement (ce n'est pas une question de ↵Gravatar herbelin2004-04-05
| | | | | | visibilité mais d'interprétation au niveau global) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5637 85f007b7-540e-0410-9357-904b9bb8a0f7
* Since coqdoc produces (X)HTML, HTML character entities can be usedGravatar sacerdot2004-04-05
| | | | | | | | | | | | in .v files. The exportation module produces generic XML ==> the character entities that were verbatim copied were never declared and the generated files were not well-formed XML files. Fixed by adding to the internal subset of the DTD an inclusion to the three files were the (X)HTML entities are defined. Due to technical reasons (HELM Getter URL rewriting), the chosen URL refers to the HELM web site. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5636 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction rapide du bug PR\#592Gravatar letouzey2004-04-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5635 85f007b7-540e-0410-9357-904b9bb8a0f7
* ** WARNING **Gravatar sacerdot2004-04-04
| | | | | | | | | | | | | | | DTD Change. ht:DEFINITION/Definition differentiated into ht:DEFINITION/Definition and ht:DEFINITION/InteractiveDefinition because of an explicit request of Iris Loeb. HELM/MoWGLI DTD and Stylesheet changed accordingly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5634 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5633 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-04-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5632 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-29 00:04:01 +0000