aboutsummaryrefslogtreecommitdiff
AgeCommit message (Collapse)Author
2000-07-25retablissement make doc et make minicoqfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@571 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-24MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@570 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@569 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des déclarationsherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@568 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-24Passage à des contextes de vars et de rels pouvant contenir des ↵herbelin
déclarations; ajout d'un mécanisme de non-vérification à la demande git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@567 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-21*) -> i*)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@566 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-21retablissement minicoq (pour Jacek)filliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@565 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-21Pattern -> parsingdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@564 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-21Fail n + appel de interpdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@563 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-21Modifs d'interpretation de patternsdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@562 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-21Modifs d'interpretation de patterns + exceptions dans le lexerdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@561 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-21Pattern -> parsingdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@560 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-20portage Refinefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@559 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-20tests Refinefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@558 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-19Quelques (*i*) pour ne pas casser oczmlwebcoq
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@557 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-05Adaptation pour Alpha.delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@556 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-05Adaptation pour alpha.delahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@555 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-04correctionmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@554 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-03ajoutsmayero
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@553 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-03Opaque pas encore implementee; syntax langage tactiquesfilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@552 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-03Traduction de syntaxe vers ltacdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@551 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-03Correction de Cofixdelahaye
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@550 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01Plus de env et sigma dans get_arity, plus de sigma dans make_arityherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@549 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01Précalcul de la forme canonique des constructeurs et arités pour traiter ↵herbelin
les cas du fichier Ensemble.v sans avoir à renormaliser à chaque fois git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@548 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01Ajout fonctions sur les aritésherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@547 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01Plus de env et sigma dans get_arity, plus de sigma dans make_arityherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@546 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01Précalcul de la forme canonique des constructeurs et arités pour traiter ↵herbelin
les cas du fichier Ensemble.v sans avoir à renormaliser à chaque fois git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@545 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01Séparation des caractères spéciaux par un blancherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@544 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01Retrait des parenthèses inutiles autour des tactiquesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@543 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01Extension de find_inductive aux co-inductifs et renommage en find_rectypeherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@542 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01Le bon type pour list_fold_right_and_leftherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@541 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01index devenu list_index échoue maintenant avec Not_found et plus Failureherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@540 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01Bug: on tentait de déclarer un schéma d'induction pour un coinductifherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@539 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-07-01Extension de find_inductive aux co-inductifs et renommage en find_rectypeherbelin
Contournement des dépendances de Rel dans les Evar pour l'inférence du prédicat (erreur "TODO4-1") git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@538 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-30fonction list_fold_left_right pas definiefilliatr
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@537 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Capture erreur de create_processherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@536 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Ajout list_fold_right_and_leftherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@535 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29MAJherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@534 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Utilisation du STRIP de config/Makefile pour gérer le mode profileherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@533 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Renommage mk_unsafe_judgment en get_judgment_of; ajout get_assumption_ofherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@532 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Séparation des contraintes de type et de valeur dans pretypingherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@531 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Relative prend sigma en plus pour la normalisation du message d'erreurherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@530 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Broutillesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@529 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Ajout make_typed_lazyherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@528 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Normalisation des Evar avant génération des erreursherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@527 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Bricolesherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@526 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Renommage mk_unsafe_judgment en get_judgment_ofherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@525 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Extension de l'inférence des types des lambdas du prédicatherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@524 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Achèvement abstraction du mécanisme (optionnel) de castherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@523 85f007b7-540e-0410-9357-904b9bb8a0f7
2000-06-29Rienherbelin
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@522 85f007b7-540e-0410-9357-904b9bb8a0f7
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 11:57:58 +0000