aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel
Commit message (Collapse)AuthorAge
* corrections de bug de la reductionGravatar barras2001-03-08
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1438 85f007b7-540e-0410-9357-904b9bb8a0f7
* compare_constr independent du groupement des applications.Gravatar barras2001-03-08
| | | | | | | ex: maintenant, eq_constr ``((f x) y)`` ``(f x y)`` = true git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1437 85f007b7-540e-0410-9357-904b9bb8a0f7
* réparation (?) discharge axiomeGravatar filliatr2001-03-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1432 85f007b7-540e-0410-9357-904b9bb8a0f7
* Re-Déplacement extended_rel_listGravatar herbelin2001-03-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1423 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement de qualid dans Nametab, hors du noyauGravatar herbelin2001-03-01
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
* nouvelle implantation de la reductionGravatar barras2001-03-01
| | | | | | | suppression de IsXtra du noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7
* retire profileGravatar mohring2001-02-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1413 85f007b7-540e-0410-9357-904b9bb8a0f7
* Changement de subst_metaGravatar mohring2001-02-28
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1412 85f007b7-540e-0410-9357-904b9bb8a0f7
* ident au lieu de string pour le nom de base de qualidGravatar herbelin2001-02-16
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1395 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un système optionnel de discharge immédiat; prise en ↵Gravatar herbelin2001-02-14
| | | | | | compte des défs locales dans les arguments des inductifs; nettoyage divers git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1381 85f007b7-540e-0410-9357-904b9bb8a0f7
* simplification du make depend; fonctions de stat. util. memoire dans ↵Gravatar filliatr2001-02-08
| | | | | | certains modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1355 85f007b7-540e-0410-9357-904b9bb8a0f7
* Chgt signature de type_of_existentialGravatar herbelin2001-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1341 85f007b7-540e-0410-9357-904b9bb8a0f7
* Retrait de EvarRef de global_reference; nettoyage autour de ast_of_refGravatar herbelin2001-02-07
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1340 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place de la possibilite d'unfolder des variables locales et des ↵Gravatar filliatr2001-01-31
| | | | | | constantes qualifiees git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1301 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'espace dans les règles d'affichage des infix si des lettres ↵Gravatar herbelin2001-01-31
| | | | | | figurent dans le token git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1297 85f007b7-540e-0410-9357-904b9bb8a0f7
* make docGravatar herbelin2001-01-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1286 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout alias mutual_inductive_path = section_pathGravatar herbelin2001-01-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1282 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout global_vars_declGravatar herbelin2001-01-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1269 85f007b7-540e-0410-9357-904b9bb8a0f7
* DocGravatar herbelin2001-01-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1267 85f007b7-540e-0410-9357-904b9bb8a0f7
* Déplacement du type stack de Reduction vers Closure et utilisation pour ↵Gravatar herbelin2000-12-26
| | | | | | 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
* Alias variable_pathGravatar herbelin2000-12-25
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1203 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug mauvais environnement dans le test d'eta-conversionGravatar herbelin2000-12-20
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1170 85f007b7-540e-0410-9357-904b9bb8a0f7
* Export de it_mkProd_or_LetIn_name et it_mkLambda_or_LetIn_nameGravatar herbelin2000-12-18
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1141 85f007b7-540e-0410-9357-904b9bb8a0f7
* Le bon choix, c'est finalement identifier = stringGravatar herbelin2000-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1132 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mise en place d'un module Ident avec test de l'efficacité quand ↵Gravatar herbelin2000-12-15
| | | | | | identifier=string git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1130 85f007b7-540e-0410-9357-904b9bb8a0f7
* - suppression mind_extract_paramsGravatar filliatr2000-12-15
| | | | | | | | | - contraintes univers parametres inductifs prises en compte - exception UniverseInconsistency donne un message "Error: Universe Inconsistency" git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1125 85f007b7-540e-0410-9357-904b9bb8a0f7
* Petite réorganisationGravatar herbelin2000-12-15
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1121 85f007b7-540e-0410-9357-904b9bb8a0f7
* Les params d'inductif deviennent en même temps propre à chaque inductif ↵Gravatar herbelin2000-12-14
| | | | | | d'un bloc et en même temps factorisés dans l'arité et les constructeurs (ceci est valable pour mutual_inductive_packet mais pas pour mutual_inductive_body); accessoirement cela permet de factoriser le calcul des univers des paramètres dans safe_typing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1113 85f007b7-540e-0410-9357-904b9bb8a0f7
* Les params d'inductif deviennent en même temps propre à chaque inductif ↵Gravatar herbelin2000-12-14
| | | | | | d'un bloc et en même temps factorisés dans l'arité et les constructeurs (ceci est valable pour mutual_inductive_packet mais pas pour mutual_inductive_body); accessoirement cela permet de factoriser le calcul des univers des paramètres dans safe_typing git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1110 85f007b7-540e-0410-9357-904b9bb8a0f7
* MAJ commentairesGravatar herbelin2000-12-14
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1101 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
* 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
* Reparation conditions de positivites inductifs, echange dans add_entryGravatar mohring2000-12-06
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1057 85f007b7-540e-0410-9357-904b9bb8a0f7
* Mini-nettoyage noms longsGravatar herbelin2000-12-05
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1048 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte de la contrainte de type dans Definition comme étant un ↵Gravatar herbelin2000-11-29
| | | | | | cast de l'utilisateur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1034 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout d'un test pour vérifier qu'on a affaire à un identGravatar herbelin2000-11-29
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1012 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
* Prise en compte du repertoire dans le section path; utilisation de dirpath ↵Gravatar herbelin2000-11-28
| | | | | | pour les noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1005 85f007b7-540e-0410-9357-904b9bb8a0f7
* Faut-il mettre la réduction let-in dans la réduction unfold ?Gravatar herbelin2000-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@991 85f007b7-540e-0410-9357-904b9bb8a0f7
* On déplie les locaux dans les types plutôt que de les quantifier par un LetGravatar herbelin2000-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@982 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
* Bug dans la gestion du contexte en présence de Fix dans le calcul de gardeGravatar herbelin2000-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@978 85f007b7-540e-0410-9357-904b9bb8a0f7
* Prise en compte des let in dans les instances de globauxGravatar herbelin2000-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@976 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au ↵Gravatar herbelin2000-11-27
| | | | | | evaluable_constant qui change de type au passage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@975 85f007b7-540e-0410-9357-904b9bb8a0f7
* Ajout map_constr_with_full_binders et strong pour SimplGravatar herbelin2000-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@973 85f007b7-540e-0410-9357-904b9bb8a0f7
* Généralisation de constant_opt_value en reference_opt_valueGravatar herbelin2000-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@971 85f007b7-540e-0410-9357-904b9bb8a0f7
* Bug dans le calcul des dépendances dans add_discharged_constantGravatar herbelin2000-11-27
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@968 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
* Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabGravatar filliatr2000-11-24
| | | | git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@947 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-22 04:57:27 +0000