aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2000-11-20Mieux à sa place dans toplevelherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@858 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Prise en compte noms longsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@857 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Ajout pr_global_reference et is_visibleherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@856 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Tables des eval_constant devient une Cstmapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@855 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Une capsule pour save_module_to dans Dischargeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@854 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-15mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@853 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-15Changed the semantics of AddRecPath.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@852 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-15methode exportfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@851 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-15-opt ne remplace plus camlp4 par camlp4o.opt car on ne peut pasfilliatr
charger de bytecode avec camlp4o.opt (et la compilation échoue sur parsing/pcoq.ml4 dans ce cas) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@850 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-15concernant les binairesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@849 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-13Retour a la version 1.1herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@848 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-11Y avait des '.' non suivis d'un séparateurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@847 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-11Gros hack pour afficher les universherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@846 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-11Code more concernant feu les abstractionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@845 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-11Prise en compte camlp4.opt dans la configuration et le Makefileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@844 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-10mise-a-jour, ajouts de quelques truc...mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@843 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-10Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@842 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-10Bugs lies a la confusion load/open et a un open abusivement recursif dans ↵herbelin
library git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@841 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-10Finalement PolyListSyntax est necessaire (la redondance venait d'une ↵herbelin
confusion dans les methodes open/load) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@840 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-10Bugs lies a la confusion load/open et a un open abusivement recursif dans ↵herbelin
library git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@839 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-09Amélioration message d'erreur arg explicité au lieu d'arg normalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@838 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-09Renommage canonique SectionLocalDecl -> SectionLocalAssumherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@837 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-09Bug et simplification nouvel Inductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@836 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-09do_Makefile -> coq_makefile pour le bootstrap!filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@835 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-09do_Makefile -> coq_makefilefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@834 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-09-I states dans les includes de Coqfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@833 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-09-I theories/Init pour faire initial.coqfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@832 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-09coqc appele avec -bindir binfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@831 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-09mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@830 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-09all_subdirs teste si son argument est un repertoire; sinon ne fait rienfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@829 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-08nouveau load pathfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@828 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-08améliorationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@827 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-08merge_locherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@826 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-08Insertion de coercion au milieu des applications partielles et propagation ↵herbelin
des contraintes de prétypage vers les sous-termes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@825 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-08First version with out_variable used. Exports all the standard librarysacerdot
without need of patches. Untested. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@824 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-08binaires a ingorer par CVSfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@823 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-08tous les binaires maintenant dans le repertoire binfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@822 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-08out_variable (Liboject.obj -> ...) distibgue de get_variablefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@821 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Modification de la table des tactic Definitions pour eviter l'ecrituremohring
de fonctions dans les .vo ajout de lemmes dans EqNat, Logic_Type suppression de PolyListSyntax qui redefinissait le Infix de append Recherche d'instances a reecrire dans les Cases et les FixPoint git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@820 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Bug sur précédent commitherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@819 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Nettoyage Names suiteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@818 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@817 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Changement/extension dans les noms de parseurs de Grammarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@816 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Correction sur commit errone de la version 1.3herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@815 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Changement/extension dans les noms de parseurs de Grammarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@814 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07Orthographeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@813 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-07MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@812 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-06Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ↵herbelin
DischargeAt) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@811 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-06print_idl inlinéherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@810 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-06MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@809 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 03:49:48 +0000