aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping
Commit message (Collapse)AuthorAge
* Bug env vis à vis du let inGravatar herbelin2000-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1129 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs calcul du prédicat des Cases et CaseGravatar herbelin2000-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1119 85f007b7-540e-0410-9357-904b9bb8a0f7
* PrinterGravatar mohring2000-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1117 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mauvais env donné à new_isevarGravatar herbelin2000-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1112 85f007b7-540e-0410-9357-904b9bb8a0f7
* Oubli test de correction à l'instantiation des evarsGravatar herbelin2000-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1111 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en pageGravatar herbelin2000-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1109 85f007b7-540e-0410-9357-904b9bb8a0f7
* LetIn dans SimplGravatar mohring2000-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1104 85f007b7-540e-0410-9357-904b9bb8a0f7
* Raffinement erreur Wrong PredicateGravatar herbelin2000-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1097 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs prise en compte du prédicat dans le Cases; le prédicat du Cases ↵Gravatar herbelin2000-12-14
| | | | | | 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
* syntaxe AST Inversion + commentaires ocamlweb autour de $Gravatar filliatr2000-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1090 85f007b7-540e-0410-9357-904b9bb8a0f7
* Hint Unfold Local + commentairesGravatar mohring2000-12-12
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1088 85f007b7-540e-0410-9357-904b9bb8a0f7
* Debut de reparation de simplGravatar mohring2000-12-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1083 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug Cases en presence d'une absence de clauseGravatar herbelin2000-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1052 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement du message d'erreur de gen_rel vers l'appelant pour le prétypageGravatar herbelin2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1011 85f007b7-540e-0410-9357-904b9bb8a0f7
* La table de pré-évaluation des constantes ne doit pas persister au dischargeGravatar herbelin2000-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@986 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de Let In pour les constantes locales, prise en compte des Let ↵Gravatar herbelin2000-11-27
| | | | | | 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
* Branchement du mécanisme d'instantiation des Evar en présence de ↵Gravatar herbelin2000-11-27
| | | | | | définitions locales vers Evarutil git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@970 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des let-in dans les fonctions de réduction pour les tactiquesGravatar herbelin2000-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@969 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de noms absolus dans la nametabGravatar herbelin2000-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@957 85f007b7-540e-0410-9357-904b9bb8a0f7
* Remplacement de certains sp_of_id par des locateGravatar herbelin2000-11-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@956 85f007b7-540e-0410-9357-904b9bb8a0f7
* certains effets disparaissent a la sortie des sections, d'autres non (selon ↵Gravatar filliatr2000-11-24
| | | | | | Summary.survive_section) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@945 85f007b7-540e-0410-9357-904b9bb8a0f7
* resolution implicites dans produits (bug)Gravatar filliatr2000-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@944 85f007b7-540e-0410-9357-904b9bb8a0f7
* print_id, print_sp -> pr_id, pr_spGravatar herbelin2000-11-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@930 85f007b7-540e-0410-9357-904b9bb8a0f7
* Abstraction du type 'qualid' pour les noms qualifiés relatifs distinct de ↵Gravatar herbelin2000-11-22
| | | | | | 'section_path' pour les noms absolus git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@919 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mieux à sa place dans toplevelGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@893 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de global_reference dans rawconstrGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@885 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de global_reference dans rawconstrGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@873 85f007b7-540e-0410-9357-904b9bb8a0f7
* Utilisation de global_reference dans rawconstr; blindage pour quand appelé ↵Gravatar herbelin2000-11-20
| | | | | | du debugger git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@872 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout erreur GlobalNotFoundGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@860 85f007b7-540e-0410-9357-904b9bb8a0f7
* Cablage des syntactif defs avec la Nametab des objetsGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@859 85f007b7-540e-0410-9357-904b9bb8a0f7
* Tables des eval_constant devient une CstmapGravatar herbelin2000-11-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@855 85f007b7-540e-0410-9357-904b9bb8a0f7
* methode exportGravatar filliatr2000-11-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@851 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bugs lies a la confusion load/open et a un open abusivement recursif dans ↵Gravatar herbelin2000-11-10
| | | | | | library git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@839 85f007b7-540e-0410-9357-904b9bb8a0f7
* merge_locGravatar herbelin2000-11-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@826 85f007b7-540e-0410-9357-904b9bb8a0f7
* Insertion de coercion au milieu des applications partielles et propagation ↵Gravatar herbelin2000-11-08
| | | | | | 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
* Nettoyage Names et conséquences (dont ajout d'un type dir_path, argument de ↵Gravatar herbelin2000-11-06
| | | | | | DischargeAt) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@811 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouveau discharge fait par le noyau; plus de recettes dans les corps des ↵Gravatar filliatr2000-11-06
| | | | | | constantes git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@807 85f007b7-540e-0410-9357-904b9bb8a0f7
* correction Abstract (et make world passe!)Gravatar filliatr2000-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@794 85f007b7-540e-0410-9357-904b9bb8a0f7
* suppression des (* open Generic *)Gravatar filliatr2000-11-02
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@793 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug Simpl avec Cases cache sous plusieurs constantesGravatar herbelin2000-10-26
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@764 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petit nettoyage de Evarutil et EvarconvGravatar herbelin2000-10-23
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@735 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug indices dans l'instance d'une evarGravatar herbelin2000-10-21
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@734 85f007b7-540e-0410-9357-904b9bb8a0f7
* Nettoyage CoercionGravatar herbelin2000-10-19
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@732 85f007b7-540e-0410-9357-904b9bb8a0f7
* Simplifications autour de typed_type (renommé types par analogie avec ↵Gravatar herbelin2000-10-18
| | | | | | sorts); documentation git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@727 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage canonique :Gravatar herbelin2000-10-18
| | | | | | | | | | | | | | declaration = definition | assumption mode de reference = named | rel Ex: push_named_decl : named_declaration -> env -> env lookup_named : identifier -> safe_environment -> constr option * typed_type add_named_assum : identifier * typed_type -> named_context -> named_context add_named_def : identifier*constr*typed_type -> named_context -> named_context git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@723 85f007b7-540e-0410-9357-904b9bb8a0f7
* Suppression d'un test inutile dans RCastGravatar herbelin2000-10-13
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@707 85f007b7-540e-0410-9357-904b9bb8a0f7
* Renommage des find_m*typeGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@698 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de Let dans build_dependent_inductiveGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@683 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug affichage du nom des letinGravatar herbelin2000-10-11
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@682 85f007b7-540e-0410-9357-904b9bb8a0f7
* Correction de bugs (alias initiaux et ordre des cas par défaut)Gravatar herbelin2000-10-10
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@679 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 05:18:57 +0000