aboutsummaryrefslogtreecommitdiff
path: root/contrib
AgeCommit message (Expand)Author
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
2002-06-03Intgration uniforme de coercions dans les dclarations (Variable and co) et re...herbelin
2002-06-03Protection des tactiques contre l'utilisation sans le bon contexte de thoriesherbelin
2002-06-03Factorisation de 'Show Programs' au premier niveau de Vernac_.commandherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-29Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vherbelin
2002-05-29Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...herbelin
2002-05-29Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.vherbelin
2002-05-15- abstract_sum_scalar, plus_sum_scalar and minus_sum_scalar were bogusbarras
2002-04-24petit bug dans les noms de fichiersletouzey
2002-04-19un thm de plus dans Zdiv; un retour chariot apres un message de la tactique F...filliatr
2002-04-18*** empty log message ***letouzey
2002-04-17jLogic.mli remplace par jolic.mliherbelin
2002-04-17Uniformisation (Qed/Save et Implicits Arguments)herbelin
2002-04-15Refine the procedure that generalizes context to current goal.huang
2002-04-15maj doc extraction dans repertoire contrib/extractionletouzey
2002-04-12maj test des realsletouzey
2002-04-12petit bug avec dummy_lamsletouzey
2002-04-11Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.mlherbelin
2002-04-10Amélioration des messages d'erreurs concernant l'inférence des implicitesherbelin
2002-04-08extraction.mlletouzey
2002-04-08babioles de renommagesletouzey
2002-04-08ajout du mange-tout d'argument en ocaml + error en Haskell pour la constante ...letouzey
2002-04-08export de la fonction Reductionops.find_conclusion pour l'extractionletouzey
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-24 13:14:26 +0000