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
...
*
* 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
*
The quoting function of the reflexive tactic is now sound: all the terms
sacerdot
2004-09-27
*
corrected bug when lhs is matched w.r.t delta
barras
2004-09-27
*
- Prise en compte de Fail n (n>0) dans plusieurs cas qui avaient
herbelin
2004-09-25
*
New: (temporary) concrete syntax to specify the morphism signature:
sacerdot
2004-09-24
*
Simplifications concommitantes à la correction du bug #855
herbelin
2004-09-24
*
Correction bug report #855
herbelin
2004-09-24
*
restructuration des printers: proofs passe avant parsing
barras
2004-09-17
*
hiding the meta_map in evar_defs
barras
2004-09-15
*
put empty_env in hint clause (vo were becoming huge!)
barras
2004-09-15
*
evar tactic bugfix
corbinea
2004-09-14
*
* The ML tactic is now also aware of rewriting directions.
sacerdot
2004-09-13
*
The ML part of the tactic now knows about covariant and contravariant morphism
sacerdot
2004-09-13
*
inclusion de meta_map dans evar_defs
barras
2004-09-12
*
simplification de clenv
barras
2004-09-10
*
Dead code removed.
sacerdot
2004-09-10
*
1. add_new_morphism now has a new optional argument that is the signature
sacerdot
2004-09-10
*
add_new_morphism has now a new argument that is the signature
sacerdot
2004-09-10
*
Add_new_morphism has now a new optional argument that is the signature of
sacerdot
2004-09-10
*
unification encore...
barras
2004-09-08
*
* cleaning/renaming in Setoids.v
sacerdot
2004-09-08
[prev]
[next]