aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
2001-05-23amelioration des messages d'erreurs vis a vis des evarsbarras
ajout automatique des chemins vers les sources au moment du Drop git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1761 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-15Modification pour passage p-automatesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1753 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-15Correction bug predicat du Cases (suite)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1752 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-12Bug propagation du predicat des Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1749 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-10Bug lift de la contrainte au passage du let (bug rapporte par S. Boulme)herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1738 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-05-03Changement de la structure des points fixesbarras
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1731 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-25Bug perte d'alias avec type dependentsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1708 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-15Bug affichage ordre des variables d'un patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1592 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-13Mise en place d'un test de clauses non utiliseesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1589 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-10Bug context incoherent au passage du lambda et du let dans evar_eqapprherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1566 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-02bug Fix signalé par Alexandre (even/odd mal interprété)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1510 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-29deux fois $Id$filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1500 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-28amelioration de la structure des universbarras
elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23amelioration de la consommation memoire de la conversion en eta-expansantbarras
les definitions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1483 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-14Alias suite + bugs divers et variésherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1466 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-14Prise en compte des Let dans l'instance des evarsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1465 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-12Rien au lieu erreur si plusieurs cas par défaut; quasi-achèvement alias ↵herbelin
dépendants git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1452 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-11Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1447 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-11Avancée vers la prise compte des alias dépendants; prise en compte des ↵herbelin
clauses par défaut dans l'ordre; amélioration messages d'erreurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1446 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-11Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1445 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-05Pb génération noms Cases + mise en place mécanisme d'histoire du filtrage ↵herbelin
pour les alias git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1422 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01nouvelle implantation de la reductionbarras
suppression de IsXtra du noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14uniformisation avec constr des lieurs dans rawterm/patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1377 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-07Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1340 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-06Ajout d'une commande pour afficher chaque coercion à la ↵herbelin
demandeparsing/g_basevernac.ml4 git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1332 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05Restructuration de classops; évolution en une version mieux intégrée au ↵herbelin
reste du système; conséquences collatérales git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1329 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-05Restructuration de classops; évolution en une version mieux intégrée au ↵herbelin
reste du système; conséquences collatérales git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1327 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-01Reparation reduce_to_mindmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1306 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-01- coqc : option -imagefilliatr
- coqmktop : manquaient des -I - tauto : rétablissement du vieux tauto en attendant la stabilité du nouveau - correction d'un bug de Simpl avec Fix (découvert dans preuve FTA) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1304 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-31Bug localisation des Syntactif Definitionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1303 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-31Mise en place de la possibilite d'unfolder des variables locales et des ↵filliatr
constantes qualifiees git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1301 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-30Prise en compte du let-in dans lookup_*_as_renamedherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1296 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et ↵herbelin
réorganisations diverses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1271 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-19Nouveaux bugs instanciation d'evar par des evarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1262 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-11Bug environnementherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1242 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-04Rajout de la restriction de l'instance en cas d'unification de 2 variables ↵herbelin
existentielles (heuristique qui existait en V6) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1235 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-03Rattrapage d'erreur pour le Case + Eval Compute in pour Definitiondelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1232 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26Bug de contextesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1224 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26Déplacement du type stack de Reduction vers Closure et utilisation pour ↵herbelin
accélérer la réduction dans Closure git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1221 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-26Pattern sera mieux dans Pretyping; relâchement head_pattern_boundherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1219 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Un nom long pour les variables de section qui font classe ou coercion; ↵herbelin
réorganisation; bugs discharge git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1201 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Bug vieux Matchherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1200 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-25Bug prédicatherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1199 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Bug prédicat old Case/Matchherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1176 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Rétablissement de l'ancien comportement de Simpl sauf dans le cas mutuel ↵herbelin
inductif où la constante la plus proche du Fix est prise en compte git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1169 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-19Export fonction testant si un inductive est un recordherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1154 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18Amélioration message d'erreur mauvais prédicatherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1142 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18Debut de nettoyage de Simplmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1140 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-23 16:21:16 +0000