index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
Commit message (
Expand
)
Author
Age
*
Wish of Maggesi implemented: the type of the morphism compatibility lemma
sacerdot
2004-10-15
*
maj
filliatr
2004-10-14
*
Bug fixed (reported by Maggesi): sometimes when the tactic had to generate new
sacerdot
2004-10-14
*
Code clean-up.
sacerdot
2004-10-14
*
reflexivity, symmetry, symmetry ... in e transitivity now fall-back
sacerdot
2004-10-14
*
maj
filliatr
2004-10-13
*
Compatibilité de Hint Rewrite avec Write State
herbelin
2004-10-13
*
maj
filliatr
2004-10-12
*
Desactivation de la construction 'lazy match' en attendant une autre solution
herbelin
2004-10-12
*
Mise en conformité de la syntaxe de Theorem/Lemma avec la doc: les lieurs so...
herbelin
2004-10-12
*
Réinstallation des lieurs avant l'énoncé de Theorem/Lemma (non documenté ...
herbelin
2004-10-12
*
Prise en compte dans cut_ident des idents de la form _23 qui sont officiellem...
herbelin
2004-10-12
*
option -no-hash-consing pour supprimmer le hash-consing
filliatr
2004-10-12
*
maj
filliatr
2004-10-11
*
'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
*
maj
filliatr
2004-10-10
*
maj
filliatr
2004-10-08
*
maj
filliatr
2004-10-07
*
setoid_symmetry in ... implemented.
sacerdot
2004-10-07
*
New commands
sacerdot
2004-10-07
*
iff and impl are now declared as transitive relations.
sacerdot
2004-10-07
*
Now Print Setoids prints also the transitivity justification of transitive
sacerdot
2004-10-07
*
maj
filliatr
2004-10-06
*
* New syntactic sugar: Add Relation ... transitivity proved by ...
sacerdot
2004-10-06
*
added transitivity
barras
2004-10-06
*
added transitivity
barras
2004-10-06
*
Add Setoid now accepts also quantified setoids.
sacerdot
2004-10-06
*
* code clean up
sacerdot
2004-10-06
*
Th unification procedure has been made a bit more complete by recording the
sacerdot
2004-10-06
*
Leibniz equality is now a quantified relation.
sacerdot
2004-10-06
*
maj
filliatr
2004-10-05
*
maj
filliatr
2004-10-05
*
* code simplification
sacerdot
2004-10-05
*
* [ bug fixed ]: when a subterm (c x1 ... xn) it is checked whether
sacerdot
2004-10-05
*
* Bug fix: in case of non dependent implications the second argument was
sacerdot
2004-10-05
*
maj
filliatr
2004-10-04
*
Added "as ..." parameter to Add Morphism.
sacerdot
2004-10-04
*
un paquet de corrections de bugs
letouzey
2004-10-04
*
maj
filliatr
2004-10-03
*
maj
filliatr
2004-10-01
*
eq_constr replaced with a conversion test where possible.
sacerdot
2004-10-01
*
1. added new parameter "as ..." to Add Setoid. Used to synthesize the name
sacerdot
2004-10-01
*
add_setoid has a new parameter used to synthesize the morphism name.
sacerdot
2004-10-01
*
Added "as ..." parameters to "Add Setoid"
sacerdot
2004-10-01
*
The "Add Setoid" command now has a new argument "as name" that is used
sacerdot
2004-10-01
*
maj
filliatr
2004-09-30
*
New tactic
sacerdot
2004-09-30
*
New tactic [setoid_]rewrite ... in ... [generate side conditions ...].
sacerdot
2004-09-30
*
Proof term size optimization: setoid_rewrite H where H is an application of
sacerdot
2004-09-30
[next]