aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-01-30Branchement sur Objdefherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1292 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-30Les Objdef introduisent une convertibilité avec les projections dans le ↵herbelin
test de conversion de Evarconv git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1291 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-30Bug fixed: the case [ id : ?1 -> ?2 |- ?] was missing in tauto_mainsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1290 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-30backtrack sur le lexeur de la V6filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1289 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-29pas de warning avec Opaque quand is_silentfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1288 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-29As an heuristic, now both in tauto and intuition we try to avoid the initialsacerdot
reduction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1287 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-27Ré-introduction des implicites à la volée dans la définition des inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1285 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-27Simplification Impargsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1284 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-27Suppression du retrait du répertoire doc de l'archive tar-gzip-éeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1283 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-27Factorisation du '.' finalherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1281 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-27make docherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1280 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-27Ré-introduction des implicites à la volée dans la définition des inductifsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1279 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-25Modif de l'axiomatisation pour enlever les /\ de _nemayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1278 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-25Remplacement d'un bug non documente par un autre documente dans ↵herbelin
quantify_extra_hyps ! git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1277 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24Ajout flush, diversherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1276 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1275 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24Protection contre l'échec de Unix.statherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1274 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et ↵herbelin
réorganisations diverses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1273 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24Prise en compte des noms longs dans les Hints et les Coercionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1272 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24Prise en compte des noms longs dans les Hints et les Coercions, et ↵herbelin
réorganisations diverses git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1271 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-24MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1270 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-24Réorganisation suite ajout de constantes locales dans les Recordsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1268 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
2001-01-24Ajout de constantes locales dans les Recordsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1266 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-22Retour en arrière sur le pb f_equal en attente meilleure solutionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1265 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-21Tests pourherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1264 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-21Bug « f_equal » : arguments inférables par une unification des types qui ↵herbelin
n'était pas faite (rem: le nouveau test ralentit un peu l'ensemble) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1263 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-19Nouveaux bugs instanciation d'evar par des evarherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1262 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-19Prise en compte de constructeurs qualifiés dans les patternsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1261 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-19Nouveau module pour centraliser les chemins des constantes globales ↵herbelin
utilisées dans le code de Coq git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1260 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-19Ajout d'un parseur d'entiers sous forme de patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1259 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-19Autour des quotations avec Casesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1258 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-19Réparation bug extensibilité de Constr.patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1257 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-19Bugs encoreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1256 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-18Bug Identity Coercionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1255 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-17MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1254 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-15Essai d'axiomatisation des numeralmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1253 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-15Ajout de commentaire coqwebmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1252 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-15Raffinementsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1251 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-14Petit bug encoreherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1250 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-14Bien sûr: bugs sur précédent commit; améliorationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1249 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-14Prise en compte de l'allocation mémoire et affichage des résultats net du ↵herbelin
surcoût de gestion du profilage git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1248 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-12Now Ring does not perform any more the same reduction twice.sacerdot
This was a logical bug of the sort_subterm function, in the sense that the aim of the function (as stated in the comment) was not to make early reductions mess with subterms; what happened, though, was that the first reduction completely removed the term and the second reduction became completely dummy. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1247 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-12Comment fixedsacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1246 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-11corr bug -mayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1245 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-11Now reduction to normal form is done only when the term is notsacerdot
in normal form. Moreover refl_eq is no more used. Instead I use sym_eqT. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1244 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-01-11Many unuseful rewritings are no more done by Ring.sacerdot
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1243 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-28 23:12:31 +0000