aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Collapse)AuthorAge
* Nom qualifié pour option -topGravatar herbelin2004-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5593 85f007b7-540e-0410-9357-904b9bb8a0f7
* Désaffectation de l'usage de Top dans Names (maintenant contrôlé dans ↵Gravatar herbelin2004-03-28
| | | | | | coqtop.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5592 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJGravatar herbelin2004-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5591 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option -top pour changer le nom 'Top' du toplevelGravatar herbelin2004-03-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5590 85f007b7-540e-0410-9357-904b9bb8a0f7
* Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ↵Gravatar herbelin2004-03-28
| | | | | | sont supposes sans dependances en les arguments des constructeurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5589 85f007b7-540e-0410-9357-904b9bb8a0f7
* Crochets pour exported les sections en xmlGravatar herbelin2004-03-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5588 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export des sections; creation COQ_XML_ROOT_LIBRARY si non existant; diversGravatar herbelin2004-03-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5587 85f007b7-540e-0410-9357-904b9bb8a0f7
* Gestion maintenant purement fonctionnelle des implicites des point-fixes; ↵Gravatar herbelin2004-03-27
| | | | | | ajout de la prise en compte dynamique des arguments scope pour les inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5586 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export compute_arguments_scope pour utilisation local a la construction des ↵Gravatar herbelin2004-03-27
| | | | | | inductifs et points fixes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5585 85f007b7-540e-0410-9357-904b9bb8a0f7
* -dead code removed.Gravatar sacerdot2004-03-27
| | | | | | | | | -latin1 is now the default in place of utf8 (since several .v files are latin1). Authomatic detection should be implemented. -fixed bug due to the wrong location of html files searched git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5584 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-03-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5583 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-03-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5582 85f007b7-540e-0410-9357-904b9bb8a0f7
* Theory file for file A.B.C.v is put in A/B/C.theory.xml.Gravatar sacerdot2004-03-26
| | | | | | | It was put in file A/B/C/C.theory.xml. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5581 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option raw-comments pour supprimer affichage de <table>Gravatar herbelin2004-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5580 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout option raw-comments pour supprimer affichage de <table>; typosGravatar herbelin2004-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5579 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ mot-clesGravatar herbelin2004-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5578 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug <BR>; ajout option raw_comment pas d'affichage de <table>; MAJ mot-clesGravatar herbelin2004-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5577 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout exportation des 'theory.xml' + diversGravatar herbelin2004-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5576 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout entree pour exporter les debuts et fins de compilation en mode -xmlGravatar herbelin2004-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5575 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout entree pour exporter les commentaires en mode -xmlGravatar herbelin2004-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5574 85f007b7-540e-0410-9357-904b9bb8a0f7
* Memorisation du type de variable (Hyp or Var)Gravatar herbelin2004-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5573 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2004-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5572 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-03-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5571 85f007b7-540e-0410-9357-904b9bb8a0f7
* Code mortGravatar herbelin2004-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5570 85f007b7-540e-0410-9357-904b9bb8a0f7
* The DTD that describes the CIC (with Explicit Named Substitutions) format.Gravatar sacerdot2004-03-25
| | | | | | | A very brief description of the DTD is in the README file. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5569 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fix and Cofix blocks with mutually defined functions having the sameGravatar sacerdot2004-03-25
| | | | | | | | | | | | | | | | name generated XML code with ambiguous names. Example: Inductive t : Set := k : t' -> t with t' : Set := k' : t -> t'. Scheme t_csc := Induction for t Sort Prop with t'_csc := Induction for t' Sort Prop. Print XML t_csc. used to show two functions both named F. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5568 85f007b7-540e-0410-9357-904b9bb8a0f7
* me = andouilleGravatar letouzey2004-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5567 85f007b7-540e-0410-9357-904b9bb8a0f7
* Selon les optims, le let-in peut avoir maintenant des argsGravatar letouzey2004-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5566 85f007b7-540e-0410-9357-904b9bb8a0f7
* Updated.Gravatar sacerdot2004-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5565 85f007b7-540e-0410-9357-904b9bb8a0f7
* ProofTree2Xml is no longer directly used by Xmlcommand.Gravatar sacerdot2004-03-25
| | | | | | | | On the contrary, it registers itself using the hook provided by Xmlcommand. The obtained designed is more modular. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5564 85f007b7-540e-0410-9357-904b9bb8a0f7
* ProofTree2Xml is no longer directly used by Xmlcommand.Gravatar sacerdot2004-03-25
| | | | | | | | On the contrary, it registers itself using the hook provided by Xmlcommand. The obtained design is more modular. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5563 85f007b7-540e-0410-9357-904b9bb8a0f7
* ProofTree2Xml is no longer directly used by Xmlcommand.Gravatar sacerdot2004-03-25
| | | | | | | | On the contrary, it registers itself using the hook provided by Xmlcommand. The obtained designed is more modular. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5562 85f007b7-540e-0410-9357-904b9bb8a0f7
* No longer used.Gravatar sacerdot2004-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5561 85f007b7-540e-0410-9357-904b9bb8a0f7
* Dead code removed.Gravatar sacerdot2004-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5560 85f007b7-540e-0410-9357-904b9bb8a0f7
* Comment removed.Gravatar sacerdot2004-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5559 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5558 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-03-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5557 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ commentairesGravatar herbelin2004-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5556 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2004-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5555 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ Claudio pour v8Gravatar herbelin2004-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5554 85f007b7-540e-0410-9357-904b9bb8a0f7
* Reparation typo de HH dans MAJ de ClaudioGravatar herbelin2004-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5553 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ Claudio pour v8Gravatar herbelin2004-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5552 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation du printer approprie a la version de syntaxeGravatar herbelin2004-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5551 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug de PP des fix (coqbugs #574)Gravatar barras2004-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5550 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2004-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5549 85f007b7-540e-0410-9357-904b9bb8a0f7
* NettoyageGravatar herbelin2004-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5548 85f007b7-540e-0410-9357-904b9bb8a0f7
* Effacement tardif de ce fichier qui a ete transforme le 5 nov 2002 en une ↵Gravatar herbelin2004-03-24
| | | | | | version non ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5547 85f007b7-540e-0410-9357-904b9bb8a0f7
* code mortGravatar herbelin2004-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5546 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvelle commande Set Extraction Flag: reglage fins des optimsGravatar letouzey2004-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5545 85f007b7-540e-0410-9357-904b9bb8a0f7
* majGravatar filliatr2004-03-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5544 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 23:35:22 +0000