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
*
un paquet de corrections de bugs
letouzey
2004-10-04
*
The "Add Setoid" command now has a new argument "as name" that is used
sacerdot
2004-10-01
*
cutrewrite does not work with relations that are not Coq-like equalities.
sacerdot
2004-09-30
*
New syntax
sacerdot
2004-09-29
*
firstorder bugfix to cope with elim of sigma types with goal is of the wrong ...
corbinea
2004-09-27
*
restructuration des printers: proofs passe avant parsing
barras
2004-09-17
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
inclusion de meta_map dans evar_defs
barras
2004-09-12
*
Ajout de or-pattern pour le match-with v8
herbelin
2004-09-09
*
The innersort is now computed as the more precise sort between the
sacerdot
2004-09-08
*
The code used to compare the synthesized and the expected type (if available)
sacerdot
2004-09-08
*
deuxieme vague de modifs: evar_defs fonctionnel
barras
2004-09-07
*
reparation des Extract Constant avec Haskell
letouzey
2004-09-06
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Ported to the new implementation of setoid_*.
sacerdot
2004-09-03
*
The old implementation of (setoid_replace c1 with c2) used to replace
sacerdot
2004-09-03
*
Application du patch de Michel Mauny pour pouvoir compiler en ocaml 3.08.1
herbelin
2004-08-24
*
Setoid_replace.setoid_replace: last argument (that was supposed to be
sacerdot
2004-07-23
*
"Show Setoids" command added.
sacerdot
2004-07-23
*
correction d'un bug de la tactique pour les semi setoid rings.
clrenard
2004-07-22
*
Protection des accès tableau car, sur Sparc-linux, cela engendre une erreur ...
herbelin
2004-07-19
*
Abstraction vis a vis du type loc pour ocaml 3.08
herbelin
2004-07-18
*
Nouvelle en-tête
herbelin
2004-07-16
*
ajout des unsafeCoerce + 2 bugs haskell
letouzey
2004-07-14
*
* <style>...</style> tag no longer generated for theory files
sacerdot
2004-07-08
*
- recent changes to doubleTypeInference.ml (that introduced double
sacerdot
2004-07-08
*
Commit to perform double type inference also on inner types.
sacerdot
2004-07-08
*
Constants just after a "Let id : t. ... Qed" local variable declaration were
sacerdot
2004-07-05
*
updated printing of evar context (may loop ?)
corbinea
2004-06-30
*
moved instantiate binding to extratactics
corbinea
2004-06-29
*
License de contrib/interface
herbelin
2004-06-29
*
contrib/interface *$*$@!
corbinea
2004-06-28
*
Modules et Records: gros changements pour prendre en compte le nouveau mind_r...
letouzey
2004-06-28
*
Licence changed from GPL to Lesser GPL.
sacerdot
2004-06-26
*
eq and eqT are the same
barras
2004-06-25
*
correspondance des records et noms de champs de records entre un module et sa...
letouzey
2004-06-25
*
Retour sur amendement de l'interprétation mult sur nat (bug 743) car incompa...
herbelin
2004-05-28
*
"comments only" commit.
coq
2004-05-13
*
Correction interprétation mult sur nat (bug 743), bug Oufo (mais Oufo est de...
herbelin
2004-05-07
*
pb install de pcoq
barras
2004-04-21
*
Copyright notice of files in contrib/xml made uniform.
sacerdot
2004-04-07
*
Old file. The new version of this script is no longer distributed with
sacerdot
2004-04-07
*
- theoryobject.dtd is the DTD for .theory files
sacerdot
2004-04-07
*
Loic code to pretty-print the generated proof-tree debranched (since it
sacerdot
2004-04-07
*
CoRN CProp detection improved: products of "sort" CProp are now recognized
sacerdot
2004-04-07
*
Coqdoc backtrack: HTML special characters are no longer quoted inside # ... #;
sacerdot
2004-04-07
*
Fake dependent products in inductive definition types are no longer replaced
sacerdot
2004-04-06
*
Important bug fix: since coqdoc is now quoting XML reserved characters in
sacerdot
2004-04-06
*
Since coqdoc produces (X)HTML, HTML character entities can be used
sacerdot
2004-04-05
*
correction rapide du bug PR\#592
letouzey
2004-04-05
[next]