index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
contrib
/
xml
Commit message (
Expand
)
Author
Age
*
Suppression IsConjecture redondant avec Conjectural
herbelin
2004-10-11
*
restructuration des printers: proofs passe avant parsing
barras
2004-09-17
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
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
*
premiere reorganisation de l\'unification
barras
2004-09-03
*
Nouvelle en-tĂȘte
herbelin
2004-07-16
*
* <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
*
Licence changed from GPL to Lesser GPL.
sacerdot
2004-06-26
*
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
*
** 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
*
Ajout exportation des 'theory.xml' + divers
herbelin
2004-03-26
*
The DTD that describes the CIC (with Explicit Named Substitutions) format.
sacerdot
2004-03-25
*
Fix and Cofix blocks with mutually defined functions having the same
sacerdot
2004-03-25
*
Updated.
sacerdot
2004-03-25
[next]