aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* bug in hashcons fun (List.for_all2 raises exn if given lists of <> lengths)Gravatar barras2004-10-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6244 85f007b7-540e-0410-9357-904b9bb8a0f7
* Amélioration message d'erreur objet de récursion de type non inductifGravatar herbelin2004-08-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6019 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nouvelle en-têteGravatar herbelin2004-07-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5920 85f007b7-540e-0410-9357-904b9bb8a0f7
* correspondance des records et noms de champs de records entre un module et ↵Gravatar letouzey2004-06-25
| | | | | | sa signature git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5823 85f007b7-540e-0410-9357-904b9bb8a0f7
* Fusion comparaison Const/Var; export is_opaqueGravatar herbelin2004-06-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5796 85f007b7-540e-0410-9357-904b9bb8a0f7
* Un bug résiduel (mais pas bien méchant) du noyauGravatar herbelin2004-05-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5767 85f007b7-540e-0410-9357-904b9bb8a0f7
* Désaffectation de l'usage de Top dans Names (maintenant contrôlé dans ↵Gravatar herbelin2004-03-28
| | | | | | coqtop.ml) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5592 85f007b7-540e-0410-9357-904b9bb8a0f7
* - fixed the Assert_failure error in kernel/modopsGravatar barras2004-02-18
| | | | | | | | | - fixed the problem with passing atomic tactics to ltacs - restructured the distrib Makefile (can build a package from the CVS working dir) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5358 85f007b7-540e-0410-9357-904b9bb8a0f7
* Inductive Types : seuls les petits types sont unitairesGravatar mohring2003-12-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5117 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug #266 (Search Error si on calcule apres avoir fait Clear d'une var Local)Gravatar barras2003-12-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5101 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar barras2003-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5006 85f007b7-540e-0410-9357-904b9bb8a0f7
* modif lexer: ident peut commencer par _Gravatar barras2003-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4991 85f007b7-540e-0410-9357-904b9bb8a0f7
* CC: added injection theoryGravatar corbinea2003-11-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4987 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout recarg_lengthGravatar herbelin2003-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4935 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression StronglyClassical, StronglyConstructive devient plus ↵Gravatar herbelin2003-11-08
| | | | | | concretement ImpredicativeSet git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4828 85f007b7-540e-0410-9357-904b9bb8a0f7
* Message inductive largeGravatar herbelin2003-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4730 85f007b7-540e-0410-9357-904b9bb8a0f7
* Set devient predicatif par defautGravatar herbelin2003-10-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4726 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un mecanisme ne chargeant pas les preuves opaquesGravatar herbelin2003-10-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4539 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction bug 328Gravatar coq2003-09-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4456 85f007b7-540e-0410-9357-904b9bb8a0f7
* message d'erreur de garde des cofixGravatar barras2003-09-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4438 85f007b7-540e-0410-9357-904b9bb8a0f7
* bug fix: term reduced in bad envGravatar barras2003-09-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4407 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place possibilité de définitions locales dans les paramètres des ↵Gravatar herbelin2003-09-06
| | | | | | inductifs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4316 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de l'opti des fermeture (mais debranche pour l'instant)Gravatar barras2003-08-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4248 85f007b7-540e-0410-9357-904b9bb8a0f7
* Improved reduction machine with closure: should use less memoryGravatar barras2003-08-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4247 85f007b7-540e-0410-9357-904b9bb8a0f7
* Comparaison de Cases module mind_equivGravatar coq2003-06-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4212 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar courant2003-06-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4209 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplification case_infoGravatar herbelin2003-06-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4124 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage CMeta en CPatVar qui sert à saisir les PMeta de PatternGravatar herbelin2003-05-19
| | | | | | | | | 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
* simplification: fst (list_chop n l) = firstn n l et snd (list_chop n l) = ↵Gravatar letouzey2003-04-16
| | | | | | list_skipn n l git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3931 85f007b7-540e-0410-9357-904b9bb8a0f7
* coupage en deux du bloc pas si mutuellement recursif des module_body & co ↵Gravatar letouzey2003-04-16
| | | | | | (...type... puis ....expr....) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3929 85f007b7-540e-0410-9357-904b9bb8a0f7
* test: un boolean et une fonction check_for_interrupt inseree dans la ↵Gravatar filliatr2003-04-08
| | | | | | 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
* *** empty log message ***Gravatar barras2003-03-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3761 85f007b7-540e-0410-9357-904b9bb8a0f7
* *** empty log message ***Gravatar courant2003-01-31
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3636 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug 'with Module' corrigeGravatar coq2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3573 85f007b7-540e-0410-9357-904b9bb8a0f7
* id_of_msid en plusGravatar letouzey2003-01-22
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3568 85f007b7-540e-0410-9357-904b9bb8a0f7
* - amelioration des messages d'erreur de la condition de gardeGravatar barras2002-12-18
| | | | | | | - restructuration de clenv.ml git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3455 85f007b7-540e-0410-9357-904b9bb8a0f7
* Contexte locale non-vide interdit a la fin d'un module ou module typeGravatar coq2002-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3453 85f007b7-540e-0410-9357-904b9bb8a0f7
* Pourquoi normaliser le prédicat du Cases dans le noyau ? (casse laGravatar herbelin2002-12-10
| | | | | | | possibilité de partage) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3416 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement du hash-consing vers declare.mlGravatar herbelin2002-12-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3412 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrections de gestion des univers et modules + meilleure gestions des ↵Gravatar coq2002-12-09
| | | | | | noms uniques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3405 85f007b7-540e-0410-9357-904b9bb8a0f7
* des Set et des Map en plusGravatar letouzey2002-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3379 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression du champ mind_singl inutilisé dans mutual_inductive_bodyGravatar letouzey2002-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3373 85f007b7-540e-0410-9357-904b9bb8a0f7
* Corrige un bug de composition de substitutionsGravatar coq2002-12-04
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3372 85f007b7-540e-0410-9357-904b9bb8a0f7
* Allègement du noyauGravatar herbelin2002-11-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3254 85f007b7-540e-0410-9357-904b9bb8a0f7
* Réforme de l'interprétation des termes :Gravatar herbelin2002-11-14
| | | | | | | | | | | | | | | - 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
* pattern-matching avec cas inutilise dans closureGravatar barras2002-10-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3148 85f007b7-540e-0410-9357-904b9bb8a0f7
* Une fonction de moins dans .mliGravatar coq2002-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3101 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lazy manuelles dans le codeGravatar coq2002-10-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3100 85f007b7-540e-0410-9357-904b9bb8a0f7
* Lazy experimentale temporaire...Gravatar coq2002-10-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3091 85f007b7-540e-0410-9357-904b9bb8a0f7
* Comparaisons des types pendant le sous-typage reactiveGravatar coq2002-09-30
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@3052 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2025-01-21 16:32:28 +0000