aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Collapse)Author
2003-11-27*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5006 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25modif lexer: ident peut commencer par _barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4991 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-25CC: added injection theorycorbinea
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4987 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-18Ajout recarg_lengthherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4935 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-11-08Suppression StronglyClassical, StronglyConstructive devient plus ↵herbelin
concretement ImpredicativeSet git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4828 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Message inductive largeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4730 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-28Set devient predicatif par defautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4726 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-10-08Mise en place d'un mecanisme ne chargeant pas les preuves opaquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4539 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-23Correction bug 328coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4456 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-22message d'erreur de garde des cofixbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4438 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-18bug fix: term reduced in bad envbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4407 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-09-06Mise en place possibilité de définitions locales dans les paramètres des ↵herbelin
inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4316 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-06Ajout de l'opti des fermeture (mais debranche pour l'instant)barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4248 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-08-05Improved reduction machine with closure: should use less memorybarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4247 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-30Comparaison de Cases module mind_equivcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4212 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-27*** empty log message ***courant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4209 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-06-10Simplification case_infoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4124 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-05-19Renommage CMeta en CPatVar qui sert à saisir les PMeta de Patternherbelin
Utilisation d'ident plutôt que int pour PMeta/CPatVar Ajout CEvar pour la saisie des Evar Pas d'entrée utilisateur pour les Meta noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4033 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-16simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = ↵letouzey
list_skipn n l git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3931 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-16coupage en deux du bloc pas si mutuellement recursif des module_body & co ↵letouzey
(...type... puis ....expr....) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3929 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-04-08test: un boolean et une fonction check_for_interrupt inseree dans la ↵filliatr
conversion pour permettre a Coq IDE d'interrompre Coq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3871 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-03-12*** empty log message ***barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-31*** empty log message ***courant
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3636 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22Bug 'with Module' corrigecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3573 85f007b7-540e-0410-9357-904b9bb8a0f7
2003-01-22id_of_msid en plusletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3568 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-18- amelioration des messages d'erreur de la condition de gardebarras
- restructuration de clenv.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3455 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-18Contexte locale non-vide interdit a la fin d'un module ou module typecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3453 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-10Pourquoi normaliser le prédicat du Cases dans le noyau ? (casse laherbelin
possibilité de partage) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3416 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-10Déplacement du hash-consing vers declare.mlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3412 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-09Corrections de gestion des univers et modules + meilleure gestions des ↵coq
noms uniques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3405 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-05des Set et des Map en plusletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3379 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-04suppression du champ mind_singl inutilisé dans mutual_inductive_bodyletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3373 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-12-04Corrige un bug de composition de substitutionscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3372 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-18Allègement du noyauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3254 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-11-14Réforme de l'interprétation des termes :herbelin
- Le parsing se fait maintenant via "constr_expr" au lieu de "Coqast.t" - "Coqast.t" reste pour l'instant pour le pretty-printing. Un deuxième pretty-printer dans ppconstr.ml est basé sur "constr_expr". - Nouveau répertoire "interp" qui hérite de la partie interprétation qui se trouvait avant dans "parsing" (constrintern.ml remplace astterm.ml; constrextern.ml est l'équivalent de termast.ml pour le nouveau printer; topconstr.ml; contient la définition de "constr_expr"; modintern.ml remplace astmod.ml) - Libnames.reference tend à remplacer Libnames.qualid git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3235 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-15pattern-matching avec cas inutilise dans closurebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3148 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-07Une fonction de moins dans .mlicoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3101 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-07Lazy manuelles dans le codecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3100 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-10-05Lazy experimentale temporaire...coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3091 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-30Comparaisons des types pendant le sous-typage reactivecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3052 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-29Activation du hash-consingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3049 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-29Hash-consing pour kernel_nameherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3048 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-29Réparation hash_consingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3047 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-09-20La notation with dependante + affichage dependante de moduels corrigecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3025 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-19La notation 'with'. L'interpretation - version preliminairecoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2975 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-19Pretty-printing preliminaire des modules, commandescoq
Print Module qid. Print Module Type qid. et affichage pendant Print All. Tout ca est preliminare, seuls les noms des composants sont affiches et non pas les corps... git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2973 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-16Strengthenning rules for modules + No modules in sectionscoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2969 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-13Renoncementherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2962 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-13Petites corrections ici et lacoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2961 85f007b7-540e-0410-9357-904b9bb8a0f7
2002-08-02Modules dans COQ\!\!\!\!coq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2957 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-01 08:25:16 +0000