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
*
Nettoyage et documentation de Library
herbelin
2005-02-06
*
Ajout printer direct cic vers xml
herbelin
2005-02-04
*
Export du printer xml vers tacinterp
herbelin
2005-02-04
*
Implemented a test for "Add [Semi] Setoid Ring" to check that the given
sacerdot
2005-02-03
*
Trivial bug fixed in "Add [Semi] Setoid Ring". An "&" in place of an "||"
sacerdot
2005-02-03
*
The statement of the compatibility theorem for addition and multiplication
sacerdot
2005-02-02
*
setoid_rewrite t; [tac]
sacerdot
2005-02-02
*
Ajout cas VernacBackTo
herbelin
2005-01-26
*
Inductive.{type_of_inductive,type_of_constructor,arities_of_specif} changed
sacerdot
2005-01-14
*
Construct "T with (Definition|Module) id := c" generalized to
sacerdot
2005-01-13
*
- Module/Declare Module syntax made more uniform:
sacerdot
2005-01-06
*
HUGE COMMIT
sacerdot
2005-01-03
*
Partie reduction_of_red_expr de tacred.ml qui dépend de la vm maintenant dan...
herbelin
2005-01-02
*
Déplacement de 'project' dans Refiner pour supprimer des dépendances en Tac...
herbelin
2005-01-01
*
Bug transformation assert dans commit précédent
herbelin
2004-12-29
*
Utilisation d'entiers en précision arbitraire pour le noyau d'omega (cf #898)
herbelin
2004-12-27
*
Remplacement du coeur d'omega (omega.ml) par la version plus gnrale utilise p...
herbelin
2004-12-27
*
Passage d'une bibliothèque de grands entiers naturels vers une bibliothèque...
herbelin
2004-12-24
*
Hugo fixed a bug of refine, and it revealed a bug of functional
coq
2004-12-10
*
Restauration type casted_open_constr pour tactique refine car l'unification n...
herbelin
2004-12-09
*
travail sur les types extraits
letouzey
2004-12-09
*
* added subst_evaluable_reference
sacerdot
2004-12-07
*
Code mort
herbelin
2004-12-06
*
Généralisation de CastedOpenConstrArg en OpenConstrArg, à charge des tacti...
herbelin
2004-12-06
*
Orthographe!
herbelin
2004-12-03
*
Correction 1.138 appliquée à tort à la branche principale au lieu de V8-0b...
herbelin
2004-11-29
*
Commit précédent erroné; retour version précédente
herbelin
2004-11-29
*
MAJ vis à vis de extratactics
herbelin
2004-11-28
*
When a reference to a constructor is met its inductive type must be closed.
sacerdot
2004-11-18
*
Locate Module
herbelin
2004-11-17
*
New command "Print Rewrite HindDb dbname".
sacerdot
2004-11-17
*
Names.substitution (and related functions) and Term.subst_mps moved to
sacerdot
2004-11-16
*
IMPORTANT COMMIT: constant is now an ADT (it used to be equal to kernel_name).
sacerdot
2004-11-16
*
Changement dans les boxed values .
gregoire
2004-11-12
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...
herbelin
2004-10-11
*
Suppression IsConjecture redondant avec Conjectural
herbelin
2004-10-11
*
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
[next]