aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Collapse)Author
2001-04-02inductifs videsfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1513 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-02ml_pop au lieu de ml_lift dans betared_astfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1512 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-04-02à fairefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1511 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30branchement extraction (bytecode seulement)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1509 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30extraction modulairefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1506 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30extraction modulaire + environnement des Fix corrigéfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1505 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30repertoire pour les tests d'extractionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1504 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30application avec bcp argsletouzey
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1503 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-30beta-reductionfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1502 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-29mise en place de Correctness (ne compile pas encore)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1501 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-28changement type_var et signaturefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1498 85f007b7-540e-0410-9357-904b9bb8a0f7
2001-03-28amelioration de la structure des universbarras
elimination des compteurs globaux de metas et d'evars du noyau nettoyage de safe_typing.ml (plus de flags) git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1497 85f007b7-540e-0410-9357-904b9bb8a0f7
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-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-26cache pour les constantesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1490 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-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-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-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-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-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-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-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-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-05indentation codefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1424 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@1419 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-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-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-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-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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-01 14:36:10 +0000