aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Collapse)Author
2004-12-30Rétablissement d'un vrai Eval sous le contexte des définitions, pas un qui ↵herbelin
réduit aussi les types du contexte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6530 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-09Amélioration message localisation constructions et modulesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6453 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-06Bug (cf #892)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6403 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-12-03Amélioration message d'erreur v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6391 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-29Complétion commit précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6381 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-26Réduire pour trouver l'arité d'une classeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6355 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-22Correction bug Notation: il faut re-déclarer les règles de parsing des ↵herbelin
notations au moment de la déclaration d'interprétation car la règle de parsing peut être dans un autre fichier qui n'est pas importé git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6340 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-22compatibility with POWERPCgregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6338 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-19Fusion OBJDEF et OBJDEF1 et renommage en CANONICAL-STRUCTUIREherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6330 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17New command "Print Rewrite HindDb dbname".sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6324 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-17Ajout 'Locate Module'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6320 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-16IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).sacerdot
MOVITATION: in a forthcoming commit the application of a substitution to a constant will return a constr and not a constant. The application of a substitution to a kernel_name will return a kernel_name. Thus "constant" should be use as a kernel name for references that can be delta-expanded. KNOWN PROBLEMS: the only problem faced is in pretyping/recordops.ml (the code that implements "Canonical Structure"s). The ADT is violated once in this ocaml module. My feeling is that the implementation of "Canonical Structure"s should be rewritten to avoid this situation. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6303 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-12*** empty log message ***gregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6296 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-12Changement dans les boxed values .gregoire
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6295 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-11-08Prise en compte des notations récursives dans l'option 'format'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6286 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-27Non affichage des notations réduites à une variableherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6258 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-20COMMITED BYTECODE COMPILERbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6245 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-17Semble raisonnable de distinguer les noms aussi dans cant_applyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6227 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-12option -no-hash-consing pour supprimmer le hash-consingfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6201 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-10-11Suppression IsConjecture redondant avec Conjecturalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6198 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-17restructuration des printers: proofs passe avant parsingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6113 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-15hiding the meta_map in evar_defsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6109 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03deplacement de clenv vers pretypingbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6058 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03premiere reorganisation de l\'unificationbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6057 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03Bug List.hd vs list_lastherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6056 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-09-03MAJ options coqtop et coqcherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6053 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-23Pas de notation v7 si purement en v8herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6023 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-23Correction bug #830 : les noms des implicites temporaires étaient inconnus ↵herbelin
au moment de l'affichage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6021 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-08-06Amélioration message d'erreur objet de récursion de type non inductifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6019 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-23"Print Setoids" command added.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5968 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-17Backtrack sur l'utilisation de pa_macro car n'existait pas en 3.06herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5941 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Abstraction vis à vis du type loc pour compatibilité ocaml 3.08herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5932 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Branchement sur pa_macro, pa_ifdef devenant obsolete en 3.08herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5931 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-16Nouvelle en-têteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-13bug #780: compilation of several units in the same coqtop processbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5900 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-07-13bug #790: better error_not_cleanbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5896 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-30updated printing of evar context (may loop ?)corbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5857 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-28Correction bug #776herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5839 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-25correspondance des records et noms de champs de records entre un module et ↵letouzey
sa signature git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5823 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-06-02Recherche de la source à partir de la gauche pour gérer des cas comme ↵herbelin
'Coercion plus : nat >-> Funclass' git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5791 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-26Affichage de la date de checkout même si pas dans le répertoire de compilationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5764 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-25Correction bug 'Time Load foo'herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5759 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-05-14test de conversion laissait echapper exception NotConvertiblebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5746 85f007b7-540e-0410-9357-904b9bb8a0f7
2004-04-17pb facto des Fixpoint + erreur avec -dump-glob et Loadbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5685 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-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-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-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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-09-29 19:28:56 +0000