aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-03-29MAJkirchner
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5601 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29Debug prints removed.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5600 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29Export Requireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5599 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29Crocret xml pour Requireherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5598 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29Commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5597 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29Typoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5596 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5595 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-28majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5594 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-28Nom qualifié pour option -topherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5593 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-28Désaffectation de l'usage de Top dans Names (maintenant contrôlé dans ↵herbelin
coqtop.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5592 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-28MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5591 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-28Ajout option -top pour changer le nom 'Top' du toplevelherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5590 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-28Passage a un 'if-then-else' ou ne sont mentionnes que les membres droits qui ↵herbelin
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
2004-03-27Crochets pour exported les sections en xmlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5588 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-27Export des sections; creation COQ_XML_ROOT_LIBRARY si non existant; diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5587 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-27Gestion maintenant purement fonctionnelle des implicites des point-fixes; ↵herbelin
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
2004-03-27Export compute_arguments_scope pour utilisation local a la construction des ↵herbelin
inductifs et points fixes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5585 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-27-dead code removed.sacerdot
-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
2004-03-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5583 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-27majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5582 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26Theory file for file A.B.C.v is put in A/B/C.theory.xml.sacerdot
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
2004-03-26Ajout option raw-comments pour supprimer affichage de <table>herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5580 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26Ajout option raw-comments pour supprimer affichage de <table>; typosherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5579 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26MAJ mot-clesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5578 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26Bug <BR>; ajout option raw_comment pas d'affichage de <table>; MAJ mot-clesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5577 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26Ajout exportation des 'theory.xml' + diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5576 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26Ajout entree pour exporter les debuts et fins de compilation en mode -xmlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5575 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26Ajout entree pour exporter les commentaires en mode -xmlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5574 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26Memorisation du type de variable (Hyp or Var)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5573 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5572 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-26majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5571 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-25Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5570 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-25The DTD that describes the CIC (with Explicit Named Substitutions) format.sacerdot
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
2004-03-25Fix and Cofix blocks with mutually defined functions having the samesacerdot
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
2004-03-25me = andouilleletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5567 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-25Selon les optims, le let-in peut avoir maintenant des argsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5566 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-25Updated.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5565 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-25ProofTree2Xml is no longer directly used by Xmlcommand.sacerdot
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
2004-03-25ProofTree2Xml is no longer directly used by Xmlcommand.sacerdot
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
2004-03-25ProofTree2Xml is no longer directly used by Xmlcommand.sacerdot
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
2004-03-25No longer used.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5561 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-25Dead code removed.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5560 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-25Comment removed.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5559 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-25majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5558 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-25majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5557 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-24MAJ commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5556 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-24*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5555 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-24MAJ Claudio pour v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5554 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-24Reparation typo de HH dans MAJ de Claudioherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5553 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-24MAJ Claudio pour v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5552 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-22 02:40:27 +0000