aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-03-05extraction termes (suite)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1426 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-05module Explore générique et réécriture EAuto avec ce module; occur check ↵filliatr
dans clenv_merge git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1425 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-05indentation codefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1424 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-05Re-Déplacement extended_rel_listherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1423 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-05Pb génération noms Cases + mise en place mécanisme d'histoire du filtrage ↵herbelin
pour les alias git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1422 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01De bizarres SR_pus_assoc au lieu de SR_plus_assocherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1421 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1420 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01Déplacement de qualid dans Nametab, hors du noyauherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1419 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01Inversion termast/astterm; suppression camldebug pour coqmktop -optherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1418 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01backtrack unification types et deplacement make_clenv_bindingfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1417 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-01nouvelle implantation de la reductionbarras
suppression de IsXtra du noyau git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1416 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-28introduction d'un refine avec resolution des types et de l'instantiation des ↵mohring
metas dans les existentielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1415 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-28modifmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1414 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-28retire profilemohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1413 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-28Changement de subst_metamohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1412 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-28Typo message Schemeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1411 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-28bug Reset et Sectionsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1410 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-27debut extraction termes; pp lambdafilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1409 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-27Ajout d'un test sur EAutomohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1408 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-27EAuto mixte (largeur puis profondeur)mohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1407 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-26ajout Vprop, Tprop et Epropfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1406 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-26changement message d'erreur Abstractfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1405 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-26Eauto version en largeurmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1404 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-26Abstract: on échoue si le but contient des existentiellesfilliatr
(corrige un ug de EAuto with zarith) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1403 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-26mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1402 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-26export open_trapping_failure pour contrib/extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1401 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-22Stringmap -> Idmapherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1400 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-22extraction des types et des inductifsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1399 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-21nouveau design ou le renommage sera fait a posteriorifilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1398 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-20mise en place fichiers extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1397 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-16Bug affichage coercionsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1396 85f007b7-540e-0410-9357-904b9bb8a0f7
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-16Tentative d'amélioration affichage decls localesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1394 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-16MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1393 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-16Suppression sp_of_idherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1392 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-16Prise en compte noms longs dans SuperAutoherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1391 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-16Prise en compte noms longs dans Implicitsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1390 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Erreur sur commitherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1389 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@1388 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Renommage des variables dans les schémas d'inductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1387 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Centralisation des références à des globaux de Coq dans Coqlib ↵herbelin
(ex-Stdlib) et suppression Stock git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1386 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Bug affichageherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1385 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1384 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1383 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Stdlib -> Coqlib, Stock disparaitherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1382 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-14Centralisation des références à des globaux de Coq dans Coqlib ↵herbelin
(ex-Stdlib) et suppression Stock git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1380 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14prise en compte des défs locales dans les arguments des inductifs; ↵herbelin
meilleure stratégie de renommage des schémas d'induction git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1379 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14Restructurationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1378 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-02-14uniformisation avec constr des lieurs dans rawterm/patternherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1377 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-08-14 23:59:17 +0000