index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
Commit message (
Expand
)
Author
Age
*
reparation d'un bug (dummy_lams -> anonym_lams) + chgmt structutr d'un ml_type
letouzey
2002-07-24
*
reparation temporaire(?) a coup de MLdummy'
letouzey
2002-07-17
*
maj
letouzey
2002-07-16
*
Pour ocamlweb
letouzey
2002-07-16
*
Souci avec example fbidon...
letouzey
2002-07-16
*
petit bug lors du passage d'hugo
letouzey
2002-07-16
*
Gros Remaniement Extraction:
letouzey
2002-07-16
*
Généralisation des syntaxes ': T := t', ':= t : T', ': T', ':= t' pour
herbelin
2002-07-11
*
Export Sumbool dans ProbBool; Reals charge et exporte ZArith_base seulement
filliatr
2002-06-21
*
ZArith_base, Zbool, Bool_nat
filliatr
2002-06-20
*
Reparation de ring pour les setoides
clrenard
2002-06-19
*
ProgWf -> Zwf
filliatr
2002-06-19
*
deplacement contrib/correctness/ProgWf -> theories/ZArith/Zwf
filliatr
2002-06-19
*
extraction vers scheme
letouzey
2002-06-07
*
Ajout d'extensions de syntaxe ARGUMENT EXTEND et VERNAC ARGUMENT EXTEND; rpar...
herbelin
2002-06-05
*
Intgration uniforme de coercions dans les dclarations (Variable and co) et re...
herbelin
2002-06-03
*
Protection des tactiques contre l'utilisation sans le bon contexte de thories
herbelin
2002-06-03
*
Factorisation de 'Show Programs' au premier niveau de Vernac_.command
herbelin
2002-06-03
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.v
herbelin
2002-05-29
*
Nouveau modèle d'analyse syntaxique et d'interprétation des tactiques et co...
herbelin
2002-05-29
*
Fichiers contrib/*/*.ml4 remplacent les contrib/*/*.v
herbelin
2002-05-29
*
- abstract_sum_scalar, plus_sum_scalar and minus_sum_scalar were bogus
barras
2002-05-15
*
petit bug dans les noms de fichiers
letouzey
2002-04-24
*
un thm de plus dans Zdiv; un retour chariot apres un message de la tactique F...
filliatr
2002-04-19
*
*** empty log message ***
letouzey
2002-04-18
*
jLogic.mli remplace par jolic.mli
herbelin
2002-04-17
*
Uniformisation (Qed/Save et Implicits Arguments)
herbelin
2002-04-17
*
Refine the procedure that generalizes context to current goal.
huang
2002-04-15
*
maj doc extraction dans repertoire contrib/extraction
letouzey
2002-04-15
*
maj test des reals
letouzey
2002-04-12
*
petit bug avec dummy_lams
letouzey
2002-04-12
*
Factorisation de quelques fonctions de clenv.ml; code mort dans coq_omega.ml
herbelin
2002-04-11
*
Amélioration des messages d'erreurs concernant l'inférence des implicites
herbelin
2002-04-10
*
extraction.ml
letouzey
2002-04-08
*
babioles de renommages
letouzey
2002-04-08
*
ajout du mange-tout d'argument en ocaml + error en Haskell pour la constante ...
letouzey
2002-04-08
*
export de la fonction Reductionops.find_conclusion pour l'extraction
letouzey
2002-04-08
*
Suppression de l'application de f_equal2 pour "mult" (non inversible);
herbelin
2002-04-05
*
mise jour
filliatr
2002-04-05
*
*** empty log message ***
huang
2002-04-04
*
Add citations
huang
2002-04-04
*
- modifs de la condition de garde pour mieux tenir compte des raisonnements
barras
2002-04-02
*
reparation du cas des arguments de type qui sont des arités + patch dummy ap...
letouzey
2002-03-28
*
Simplification de Proof_type.prim_rule
herbelin
2002-03-27
*
Refonte complete de la génération des types ML
letouzey
2002-03-26
*
An intuitionistic first-order theorem prover -- JProver.
huang
2002-03-22
*
reparation du test des reals
letouzey
2002-03-21
*
considerations de pretty-print
letouzey
2002-03-21
*
deux fichiers supplementaires de customisation d'extraction
letouzey
2002-03-21
[next]