aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2000-11-28-I inutiles pour coqc et utilisation de -R theories (pour garder trace des ↵herbelin
noms de repertoire git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1002 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-28Elimination du 'delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1001 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-28Elimination du 'delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1000 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-28Un == non reconnu sous alphadelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@999 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-28Rajout de PolyListSyntax aussi dans Makefileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@998 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Distinction local/globalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@997 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Bug affichage inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@996 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Xml contrib retachedsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@995 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Many improvements. Xml contrib retached to the V7.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@994 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27uniformisation messages d'erreurfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@993 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27load_module / open_module un tantinet plus rapidesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@992 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-27Remettre une section dans fast_integer pour contourner un bug de définition ↵herbelin
locale git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@990 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27La bonne modif des Unfoldherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@989 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@988 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Bug dans find_common_hyps_then_abstract en présence de défs localesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@987 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-27Bug extract_instance en présence de défs localesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@985 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Prise en compte des définitions localesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@984 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-27Prise en compte des implicites de locaux à l'affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@983 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-27Suppression de Unfold inutile et maintenant échouantherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@981 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@980 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-27Branchement des Local sur des SectionLocalDefherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@977 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-27Affichage des définitions localesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@974 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-27Changement du parseur par défaut dans Syntaxherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@972 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-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-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-26Nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@967 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Appel des constantes globaux par des noms absolusherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@966 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Le nouvel Induction s'appelle NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@965 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@964 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Prise en compte qualidherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@963 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Restruration autour de qualidargherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@962 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Calcul du chemin optimal dans qualid_of_globalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@961 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Distinction claire entre Induction (nom interne : raw_induct) et le nouvel ↵herbelin
induction (now temporaire NewInduction) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@960 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Prise en compte noms longs dans divers fonctions de Printherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@959 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-26Prise en compte de noms absolus dans la nametab + nettoyageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@958 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-26sp au lieu de id dans END-SECTIONherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@955 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@954 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-11-24Bug relocation des hypothèses quand les contextes de définitions et ↵herbelin
d'utilisation diffèrent git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@953 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 19:30:00 +0000