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
*
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
*
Mise en conformité de Derive Inversion et Derive Dependent Inversion avec la...
herbelin
2004-11-15
*
Changement dans les boxed values .
gregoire
2004-11-12
*
Added code to get rid of duplicate rewriting rules.
sacerdot
2004-10-28
*
Ajout 'dependent rewrite in'
herbelin
2004-10-28
*
Factorisation cut_replacing
herbelin
2004-10-27
*
Restructuration fonctions de réécriture depuis égalité dépendante
herbelin
2004-10-27
*
Restructuration fonctions de réécriture depuis égalité dépendante; facto...
herbelin
2004-10-27
*
Word "setoid" banned from the error messages. "relation" used instead.
sacerdot
2004-10-25
*
Missing check implemented (closes a bug from Bas Spitters).
sacerdot
2004-10-25
*
The morphism lemma type was simplified only in modules and not in module
sacerdot
2004-10-21
*
Error message improved.
sacerdot
2004-10-21
*
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
[next]