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
*
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
*
** WARNING **
sacerdot
2004-04-04
*
LocalFact added as a choice for the "as" attribute of ht:VARIABLE in the
sacerdot
2004-04-01
*
Big bug fixed: interactive local definitions where handled as constants
sacerdot
2004-04-01
*
Output of theory files reimplemented using Buffer.
sacerdot
2004-04-01
*
~keep_sections was now redundant. Got rid of.
sacerdot
2004-04-01
*
En mode batch, recuperation via Declare de l'information si un inductive est ...
herbelin
2004-03-31
*
Fake dependent types in constructors of inductive types are now preserved.
sacerdot
2004-03-31
*
*** WARNING: DTD Change ***
sacerdot
2004-03-30
[next]