aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Collapse)Author
2002-01-16correction de bug avec les mutuels imbriques a plusieurs niveauxbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2401 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-20Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2353 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Bug de de Bruijn pour le LetInherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2348 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19Le cas LetIn avait été oublié dans case_branches_specifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2324 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-19reparation de make doc (ocamlweb & _)letouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2321 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-13compat ocaml 3.03filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2291 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-10- condition de garde (suite)barras
- commande Back git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2283 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-12-04bug fix de la condition de gardebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2264 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-30desobfuscation du code de la verif de la condition de gardebarras
reparation bug de la tactique CutRewrite git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2261 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-29reparation de Locatebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2247 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-29nouvel algo de conversion plus uniformebarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2246 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Amélioration messages d'erreur arité incorrecte (notamment record)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2236 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-21Oubli des contraintes d'univers lors de la suppression des cast dans un ↵herbelin
commit précédent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2227 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Ajout isEvarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2220 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Ajout mkArityherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2218 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Fusion de declare/add_constant, declare/add_parameter et add_discharged_constantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2211 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20types vs constrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2210 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Suppression des Cast externes dans les définitionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2208 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-20Ajout quelques fonctions; code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2206 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-19Mise en place d'une méthode directe pour indiquer le type des déclarations ↵herbelin
à toplevel plutôt que de passer par mkCast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2203 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-12Suites modifs du noyau. Univ devient purement fonctionnel.barras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2183 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-09MAJ pour make docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2177 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-08Rétablissement de la persistance des Cast; typage des LetIn sans recours à ↵herbelin
Cast git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2171 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-06corrections mineures suite au commit de restructuration du noyaubarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2165 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-11-05GROS COMMIT:barras
- reduction du noyau (variables existentielles, fonctions auxiliaires pour inventer des noms, etc. deplacees hors de kernel/) - changement de noms de constructeurs des constr (suppression de "Is" et "Mut") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2158 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-17Abstraction de l'immplementation de dirpath et implementation dans l'autre ↵herbelin
sens pour plus de partage entre chemins git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2126 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-12Déplacement de global_reference dans Names pour pouvoir lier Nametab à ↵herbelin
grammar.cma git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2112 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-11Suppression option immediate_discharge; nettoyage de Declare et conséquencesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2109 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-09Suppression des arguments sur les constantes, inductifs et constructeursbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2106 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-03Bugs de vérification de la bonne fondation en présence de définitions ↵herbelin
locales dans le type de l'inductif décroissant git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2099 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-10-03Correction messages d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2096 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-21repare la perte d'opacite a la fermeture de sectionbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2050 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Transparentbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2035 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Nettoyage des commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2031 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Compatibilté make docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2030 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-20Romegamohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2014 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Type 'sorts_family' (ex elimination_sorts) pour caractériser les familles ↵herbelin
des sortes (InProp, InSet, InType) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2009 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-19Affichage des dir_path videherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2006 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-18Romega/names/Makefilemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1980 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-14exceptionsbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1965 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-14mauvais rattrapage d'exceptionbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1964 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-10Utilisation d'un type spécifique (elimination_sorts) pour caractériser les ↵herbelin
éliminations, pour éviter les collisions avec les univers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1944 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Passage aux univers algébriquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1941 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Passage aux univers algébriquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1940 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Suppression de Type_1, inutile, et non prévu dans le modèle des univers ↵herbelin
algébriques git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1937 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Mécanisme pour faire remonter les contraintes de typage sur les variables ↵herbelin
de section au niveau du discharge, sans avoir à garder tout l'environnement de la section; suppression retypage du type des constantes déchargées git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1935 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-09Mécanisme pour faire remonter les contraintes de typage sur les variables ↵herbelin
de section au niveau du discharge, sans avoir à garder tout l'environnement de la section git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1934 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-07Extension à Cases et Fix de la réduction pas à pas vers un produit (Red)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1928 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-05Version de la reduction dans Closure plus econome en memoire:barras
- la pile ne contient plus les arguments appliques deja consommes - ajout d'un "lock" sur les glacons en cours de calcul git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1922 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-09-04erreur de pretty-print lors de l'affichage de termes avec de Bruijn non liesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1920 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-28 08:43:35 +0000