aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2000-12-20Bug dans l'utilisation de l'option debugherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1165 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Import module force l'ouverture du module même s'il était déjà ouvert ↵herbelin
afin de pouvoir re-rendre visible des noms ayant été cachés depuis l'ouverture du module; renommage de open_module en import_module avec cette nouvelle spéc git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1164 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Bug norm_evar_pf; remplacement par l'insertion d'un noeud local_constraints ↵herbelin
qui fait l'instantiation des evars git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1163 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Ajout set_lcherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1162 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Scripts de correction d'uriherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1161 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1160 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-20Non verbose par défautherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1159 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-19Correction pour les variables abstraites dans les Tactic Definitionsdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1158 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-19DEMOS passe et MUTUAL-EXCLUSION aussi modulo Realizerdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1157 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-19correction de bugs sur commit précédentherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1156 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-19Découpage des différentes fonctionnalités de build_mutual et ↵herbelin
definition_structure + export des sous-fonctions git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1155 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-19Amélioration affichage Print ALlherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1153 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-19Pédagogieherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1152 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-19Correction associativite de Repeat/Orelsedelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1151 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-19AutoRewrite n'ecrit plus de valeurs fonctionnelles sur disquedelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1150 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18Bugs connus et non résolusherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1149 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1148 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18Renommages autour de NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1147 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18Code mortherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1146 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18Documentationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1145 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18Suppression de l'affichage des instances des ?nherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1144 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1143 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-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-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-18Mise a jourmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1139 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-18Mise a jourmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1138 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-16MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1137 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-16Redondant or incompatible instantiations in clenv_assign now correctly trappedherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1136 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-16*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1135 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-16Prise en compte modules/sections qualifiés dans SearchPattern et SearchRewriteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1133 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 pageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1131 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-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-15pb niveaumayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1128 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15suppression warning et calcule type dans replace_by_meta dans tous les casfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1127 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1126 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-15MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1124 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Réparation de bugs de LoadPathherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1123 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-12-15Re-ajout des syntaxes Add LoadPath, Remove LoadPath, etc; ajout entrées ↵herbelin
'Set Implicit Arguments' and co git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1122 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-15Bug des locaux au premier niveau des modules qui disparaissaient de ↵herbelin
l'environnement (changement de is_section_p) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1120 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-15Mise a jourmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1118 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-15test univers, inductifs et sectionsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1116 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 18:33:45 +0000