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 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
*
declare_internal_constant behaved as declare_constant for proofs (e.g.
sacerdot
2004-03-30
*
No longer used (and probably no longer working) code removed.
sacerdot
2004-03-30
*
Added a <br/> after "Require ...".
sacerdot
2004-03-30
*
syntax error: dandling in
sacerdot
2004-03-30
*
Renommage
herbelin
2004-03-30
*
2 choix incorrects
herbelin
2004-03-30
*
Distinction entre declarations internes (p.ex. _subproof) et declarations uti...
herbelin
2004-03-30
*
Fabrication de l'uri a partir du path utilisateur
herbelin
2004-03-30
*
Retrait debogage
herbelin
2004-03-29
*
Export du type de preuve en cours pour xml
herbelin
2004-03-29
*
Debug prints removed.
sacerdot
2004-03-29
*
Export Require
herbelin
2004-03-29
*
Export des sections; creation COQ_XML_ROOT_LIBRARY si non existant; divers
herbelin
2004-03-27
*
-dead code removed.
sacerdot
2004-03-27
*
Theory file for file A.B.C.v is put in A/B/C.theory.xml.
sacerdot
2004-03-26
[next]