aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2001-03-27conservation des arguments dans Prop (snif)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1495 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-27mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1494 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-27extraction recursive d'un morceau d'environnementfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1493 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-27trace des inductifs sur Propletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1492 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-26Bibliotheque Nummohring
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1491 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-26cache pour les constantesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1490 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-25ocaml 3.01 requisherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1488 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-25Tag pour une beta3-ocaml3.01herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1487 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1486 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1485 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23Les règles d'affichage ajoutés dans le commit précédent avait le même ↵herbelin
nom que la règle pour command git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1484 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23amelioration de la consommation memoire de la conversion en eta-expansantbarras
les definitions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1483 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23mise a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1482 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23eta-expansion des constructeurs si necessaire (a posteriori en miniML)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1481 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23La strategie de recherche de lookup_eliminator etait insuffisanteherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1480 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-23suppression des param dans inductifs. suite du Casesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1479 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-22Règle de syntaxe pour CASTEDCOMMANDherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1478 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-22Problèmes de NewInductionherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1477 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-22Bug MUTCASE au lieu CASEherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1476 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-21Reecriture du extract_type pour Prod et Lambda. Eta-expansion dans les ↵letouzey
branches des Cases (cf sumbool_rec) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1475 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-21option -verbose a coqc; option -i suppriméefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1474 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-20affichage declarations fix + bug extraction sumbool_rec mis a jourfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1473 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-20mlutilfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1472 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-20extraction naive de fix et casefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1471 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-20Extract_term_with_type. mise a jour & verification des commentairesletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1470 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15entetesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1469 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-15les options passées sont prioritaires sur les -I par défautfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1468 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-14MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1467 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-14Alias suite + bugs divers et variésherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1466 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-14Prise en compte des Let dans l'instance des evarsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1465 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-14interface du extract_rec. Extract_constr prend un environnementletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1464 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-14*** empty log message ***herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1463 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-14Ajout syntaxe zarithherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1462 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-14MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1461 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-13passage ocaml 3.01filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1460 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-13signatures dans le bon ordrefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1459 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-13Finitefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1458 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-13simplification: plus de contexte pour extract_type et contexte simplifié ↵filliatr
pour extract_term git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1457 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-13suite de la verification des assert falseletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1456 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-12Amélioration message d'erreur conditions de gardeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1455 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-12MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1454 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-12Ajout list_map3herbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1453 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-12Rien au lieu erreur si plusieurs cas par défaut; quasi-achèvement alias ↵herbelin
dépendants git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1452 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-12fin du letinletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1451 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-12debut let infilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1450 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-12mise a jour commentaires'filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1449 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-12Commentaires. Verification des assert false. Probleme des types ML arity.letouzey
Correction des dependances pour bin/coq-extraction dans le Makefile git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1448 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-11Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1447 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-11Avancée vers la prise compte des alias dépendants; prise en compte des ↵herbelin
clauses par défaut dans l'ordre; amélioration messages d'erreurs git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1446 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-11Déplacement des erreurs non noyau dans Pretype_errors ou Cases; localisationherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1445 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 20:30:43 +0000