aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2004-04-04** WARNING **sacerdot
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
2004-04-02majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5633 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-01majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5632 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-01majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5631 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-01LocalFact added as a choice for the "as" attribute of ht:VARIABLE in thesacerdot
DTD. Used for local proofs (e.g. "Let x : True. auto. Qed."). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5630 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-01Big bug fixed: interactive local definitions where handled as constantssacerdot
and not as variables. Partially fixed. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5629 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-01Output of theory files reimplemented using Buffer.sacerdot
This avoids stdout cluttering in interactive mode. Whenever verbose is set to true, all the strings sent to the Buffer are also printed on stdoud. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5628 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-01~keep_sections was now redundant. Got rid of.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5627 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-31majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5626 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-31majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5625 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-31Morphismes déclarés comme Lemma pas comme Definitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5624 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-31En mode batch, recuperation via Declare de l'information si un inductive est ↵herbelin
un record; restructuration en consequence git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5623 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-31Export de l'information si un inductive est un record ou non (pour xml)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5622 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-31Fake dependent types in constructors of inductive types are now preserved.sacerdot
The idea is: 1. constructors are always declare by hand by the user ==> binders always have a meaning. 2. the binders are fundamental for record fields, even if the dependent product is really non-dependent. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5621 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5620 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30*** WARNING: DTD Change ***sacerdot
@name of ht:SECTION renamed in @uri Its semantics has not changed (it is the base URI of relative URIs defined inside the section). HELM/MoWGLI stylesheets updated accordingly. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5619 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30The XML exportation hook for require is now active for:sacerdot
- Require id. - Require Export id. - Require "file". - Require Export "file". git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5618 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30declare_internal_constant behaved as declare_constant for proofs (e.g.sacerdot
*_subproof) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5617 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30Heuristique pour traduire if-then-else quand le re-typage echoueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5616 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30Distinction entre declarations internes (p.ex. _subproof) et declarations ↵herbelin
utilisateurs pour export xml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5615 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30No longer used (and probably no longer working) code removed.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5614 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30Added a <br/> after "Require ...".sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5613 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30syntax error: dandling insacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5612 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30Renommageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5611 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-302 choix incorrectsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5610 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30Distinction entre declarations internes (p.ex. _subproof) et declarations ↵herbelin
utilisateurs pour export xml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5609 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-30Fabrication de l'uri a partir du path utilisateurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5608 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5607 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29majfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5606 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29Retrait debogageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5605 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29Export du type de preuve en cours pour xmlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5604 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29tools/coq_vo2xml removed since no longer in use.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5603 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-03-29"xml" target removed from generated makefiles (since it was no longer used)sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5602 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 03:51:06 +0000