index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
Commit message (
Expand
)
Author
Age
*
COMMITED BYTECODE COMPILER
barras
2004-10-20
*
The bug already closed in revision 1.90 was reintroduced again.
sacerdot
2004-10-20
*
Proof term size reduction (again).
sacerdot
2004-10-19
*
* Code simplification and clean-up. In particular there is no more code
sacerdot
2004-10-18
*
Code simplification and clean-up.
sacerdot
2004-10-18
*
The lem field was not computed properly for morphisms whose argument was
sacerdot
2004-10-18
*
The "lem" field of a morphism used to be the compatibility proof, but it
sacerdot
2004-10-18
*
Bug fixed: relations quantified more than once where abstracted in the wrong
sacerdot
2004-10-18
*
More informative error message when the tactic tries to generate a new
sacerdot
2004-10-18
*
zeta flag added to reduce LetIns in a morphism type. Morphisms with local
sacerdot
2004-10-18
*
Wrong comment committed. The tactic behaves correctly only when the
sacerdot
2004-10-15
*
Wish of Maggesi implemented: the type of the morphism compatibility lemma
sacerdot
2004-10-15
*
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
*
Compatibilité de Hint Rewrite avec Write State
herbelin
2004-10-13
*
'match term' now evaluates by default. Added 'lazy' keyword to delay the eval...
herbelin
2004-10-11
*
setoid_symmetry in ... implemented.
sacerdot
2004-10-07
*
New commands
sacerdot
2004-10-07
*
Now Print Setoids prints also the transitivity justification of transitive
sacerdot
2004-10-07
*
* New syntactic sugar: Add Relation ... transitivity proved by ...
sacerdot
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
*
* 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
*
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
*
The "Add Setoid" command now has a new argument "as name" that is used
sacerdot
2004-10-01
*
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
*
cutrewrite does not work with relations that are not Coq-like equalities.
sacerdot
2004-09-30
*
setoid_replace E1 with E2
sacerdot
2004-09-30
*
* error messages improved
sacerdot
2004-09-29
*
Add Relation is now able to detect non well typed relation registrations.
sacerdot
2004-09-29
*
The Add Morphism command is now able to detect in advance:
sacerdot
2004-09-29
*
New syntax
sacerdot
2004-09-29
*
The Prod special case works only when the premise is of type Prop.
sacerdot
2004-09-29
*
1. major code clean-up for the Prod case
sacerdot
2004-09-29
*
impl is a reflexive relation (it used to be areflexive).
sacerdot
2004-09-29
*
1) bug fixed: new goals where compared according to the relation arguments
sacerdot
2004-09-29
*
The list of possible solutions proposed by the tactic cannot contain any
sacerdot
2004-09-29
*
Hugly temporary notation
sacerdot
2004-09-29
*
The quoting function is now 100% complete.
sacerdot
2004-09-29
*
The quoting function is now almost complete (in the sense that it can find
sacerdot
2004-09-28
[next]