aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
2002-11-15Passage à une représentation des fixpoints plus primitive dans constr_expr ...herbelin
2002-11-14Réforme de l'interprétation des termes :herbelin
2002-11-14MAJ syntaxeherbelin
2002-11-13typocourant
2002-11-12rep why ignorefilliatr
2002-11-05Intégration de la branche mowgliherbelin
2002-11-05Intégration des modifs de la branche mowgli :herbelin
2002-11-05cosmetiqueletouzey
2002-11-04un bug concernant l'expansion des Map_rec si Map n'est pas ouvertletouzey
2002-11-04nettoyage et reorganisationletouzey
2002-11-04maj avec tous les mliletouzey
2002-11-04Un fichier a utiliser via Drop pour le debug de l'extraction.letouzey
2002-10-31L'extraction c'est magic cvs -n upletouzey
2002-10-28Des critères plus fins d'analyse des implicites automatiques; meilleur affic...herbelin
2002-10-23Clarification changements autour de Remark/Fact/Localherbelin
2002-10-23Omega échouait à effacer les hypothèses à contenu arithmétique lorsque c...herbelin
2002-10-19Meilleure lisibilité grâce à tclTHENLISTherbelin
2002-10-19Réparation bug #180herbelin
2002-10-14TacCall attend une référenceherbelin
2002-10-14Ajout "Arguments Scope" pour associer des "scopes" aux arguments d'uneherbelin
2002-10-13Mise en place de 'Scope' pour gérer des ensembles de notations - phase 1; ha...herbelin
2002-10-07Lazy manuelles dans le codecoq
2002-10-06correcting the treatment of many tactics that use quant_hyp in file xlate.mlbertot
2002-10-05Lazy experimentale temporaire...coq
2002-10-04Re-introduce the treatement of Tacticals that Hugo had already done inbertot
2002-10-03Previous version did compile but did not make it possible to actually runbertot
2002-10-02Omega can now elim hyps of type False. Therefore, it knows how to dealcourant
2002-10-01Adding the congruence closure tactics (CC and CCsolve).corbinea
2002-09-29Complétion filtrageherbelin
2002-09-24Un peu (plus) d'ordre dans Nametab...coq
2002-09-24suite chgt liés aux modulesletouzey
2002-09-19portage Correctness (substitutivité pour les modules)filliatr
2002-09-18retablissement de Correctness (pas encore teste' cependant)filliatr
2002-08-17Suppression automatique du corps des définitions locales opaques dansherbelin
2002-08-02Modules dans COQ\!\!\!\!coq
2002-07-24reparation d'un bug (dummy_lams -> anonym_lams) + chgmt structutr d'un ml_typeletouzey
2002-07-17reparation temporaire(?) a coup de MLdummy'letouzey
2002-07-16majletouzey
2002-07-16Pour ocamlwebletouzey
2002-07-16Souci avec example fbidon...letouzey
2002-07-16petit bug lors du passage d'hugoletouzey
2002-07-16Gros Remaniement Extraction:letouzey
2002-07-11Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pourherbelin
2002-06-21Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulementfilliatr
2002-06-20ZArith_base, Zbool, Bool_natfilliatr
2002-06-19Reparation de ring pour les setoidesclrenard
2002-06-19ProgWf -> Zwffilliatr
2002-06-19deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwffilliatr
2002-06-07extraction vers schemeletouzey
2002-06-05Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...herbelin
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-05 04:39:31 +0000