aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-03-08changement comparaison etatsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1436 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-07distinction contexte et signaturefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1435 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-06plus de commentairesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1434 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-06on gele apres un Require => meilleures performances memoire, en particulier ↵filliatr
pour Proof General git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1433 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-06réparation (?) discharge axiomefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1432 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-06Modification de e_give_exact pour eviter d'echouer sur l'unificationmohring
en l'absence de variables existentielles git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1431 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-06eta-expansionmohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1430 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-06EAutod (debug)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1429 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-06modifs pour extraction; bug coqmktopfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1428 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-05ocamlwebfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1427 85f007b7-540e-0410-9357-904b9bb8a0f7
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 06:36:01 +0000