aboutsummaryrefslogtreecommitdiff
path: root/kernel
AgeCommit message (Collapse)Author
2001-02-16ident au lieu de string pour le nom de base de qualidherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1395 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Mise en place d'un système optionnel de discharge immédiat; prise en ↵herbelin
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
2001-02-08simplification du make depend; fonctions de stat. util. memoire dans ↵filliatr
certains modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1355 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-07Chgt signature de type_of_existentialherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1341 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-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-31Ajout d'espace dans les règles d'affichage des infix si des lettres ↵herbelin
figurent dans le token git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1297 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-27make docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1286 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-27Ajout alias mutual_inductive_path = section_pathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1282 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24Ajout global_vars_declherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1269 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24Docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1267 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-25Alias variable_pathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1203 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Bug mauvais environnement dans le test d'eta-conversionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1170 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18Export de it_mkProd_or_LetIn_name et it_mkLambda_or_LetIn_nameherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1141 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Le bon choix, c'est finalement identifier = stringherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1132 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Mise en place d'un module Ident avec test de l'efficacité quand ↵herbelin
identifier=string git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1130 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15 - suppression mind_extract_paramsfilliatr
- 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
2000-12-15Petite réorganisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1121 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-14Les params d'inductif deviennent en même temps propre à chaque inductif ↵herbelin
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
2000-12-14Les params d'inductif deviennent en même temps propre à chaque inductif ↵herbelin
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
2000-12-14MAJ commentairesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1101 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-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-06Reparation conditions de positivites inductifs, echange dans add_entrymohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1057 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-05Mini-nettoyage noms longsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1048 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Prise en compte de la contrainte de type dans Definition comme étant un ↵herbelin
cast de l'utilisateur git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1034 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-29Ajout d'un test pour vérifier qu'on a affaire à un identherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1012 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-28Prise en compte du repertoire dans le section path; utilisation de dirpath ↵herbelin
pour les noms de modules git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1005 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Faut-il mettre la réduction let-in dans la réduction unfold ?herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@991 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27On déplie les locaux dans les types plutôt que de les quantifier par un Letherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@982 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-27Bug dans la gestion du contexte en présence de Fix dans le calcul de gardeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@978 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Prise en compte des let in dans les instances de globauxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@976 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Ajout de evaluable_named_decl et evaluable_rel_decl en parallele au ↵herbelin
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
2000-11-27Ajout map_constr_with_full_binders et strong pour Simplherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@973 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Généralisation de constant_opt_value en reference_opt_valueherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@971 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Bug dans le calcul des dépendances dans add_discharged_constantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@968 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-24Ajout objets END-SECTION pour les nametabs + nettoyage lib/nametabfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@947 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-23Affichage des paths avec des '.', print_id -> pr_id, print_sp -> pr_spherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@929 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Ajout push_rels_assumherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@922 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-23Reparation IsMutConstruct + Transparentmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@920 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-22deplacement poly_args; iterateurs sur les segmentsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@917 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-22Reparation bug mutuels indmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@916 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21Ajout d'une fonction pour recuperer la liste des constantesdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@910 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-21implicites manuelsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@905 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-07 02:54:39 +0000