aboutsummaryrefslogtreecommitdiff
path: root/pretyping
AgeCommit message (Collapse)Author
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
2000-12-16Suppression du warning several default clausesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1134 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Bug env vis à vis du let inherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1129 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Bugs calcul du prédicat des Cases et Caseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1119 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Printermohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1117 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Mauvais env donné à new_isevarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1112 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Oubli test de correction à l'instantiation des evarsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1111 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Mise en pageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1109 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14LetIn dans Simplmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1104 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Raffinement erreur Wrong Predicateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1097 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Bugs prise en compte du prédicat dans le Cases; le prédicat du Cases ↵herbelin
devient systématiquement dépendent; blindage de certaines erreurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1096 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-12syntaxe AST Inversion + commentaires ocamlweb autour de $filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-12Hint Unfold Local + commentairesmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1088 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-11Debut de reparation de simplmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1083 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-05Bug Cases en presence d'une absence de clauseherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1052 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1011 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27La table de pré-évaluation des constantes ne doit pas persister au dischargeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@986 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Utilisation de Let In pour les constantes locales, prise en compte des Let ↵herbelin
In dans le discharge, l'unification de evarconv et l'unification de clenv git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@979 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Branchement du mécanisme d'instantiation des Evar en présence de ↵herbelin
définitions locales vers Evarutil git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@970 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Prise en compte des let-in dans les fonctions de réduction pour les tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@969 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Prise en compte de noms absolus dans la nametabherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@957 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Remplacement de certains sp_of_id par des locateherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@956 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24certains effets disparaissent a la sortie des sections, d'autres non (selon ↵filliatr
Summary.survive_section) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@945 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24resolution implicites dans produits (bug)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@944 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23print_id, print_sp -> pr_id, pr_spherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@930 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de ↵herbelin
'section_path' pour les noms absolus git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Mieux à sa place dans toplevelherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@893 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Utilisation de global_reference dans rawconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@885 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Utilisation de global_reference dans rawconstrherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@873 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Utilisation de global_reference dans rawconstr; blindage pour quand appelé ↵herbelin
du debugger git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@872 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Ajout erreur GlobalNotFoundherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@860 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-20Cablage des syntactif defs avec la Nametab des objetsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@859 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-15methode exportfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@851 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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-14 06:35:20 +0000