index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
equality.ml
Commit message (
Expand
)
Author
Age
*
Add a flag to control betaiota reduction during unification to maintain backw...
msozeau
2011-04-18
*
- Add modulo_delta_types flag for unification to allow full
msozeau
2011-03-13
*
Fixing injection bug #2493 (regression introduced by fixing injection
herbelin
2011-03-05
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Delayed the evar normalization in error messages to the last minute
herbelin
2010-11-07
*
correction of bug #2414 (report of r 13586)
jforest
2010-10-27
*
Added eta-expansion in kernel, type inference and tactic unification,
herbelin
2010-09-20
*
In the computation of missing arguments for apply, accept that the
herbelin
2010-09-17
*
Fix unescaped end-of-lines (OCaml warning 29)
glondu
2010-09-13
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New pass on inductive schemes
herbelin
2010-05-29
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
*
Improving compatibility between 8.2 and 8.3
herbelin
2010-04-05
*
Applied greenrd's patch to fix bug 2255 (injection failed to
herbelin
2010-03-27
*
Safer, though ad hoc, approach to re-interpretation of the argument of
herbelin
2009-12-28
*
Generic support for open terms in tactics
herbelin
2009-12-21
*
Improved strategy for rewriting lemma possibly depending because of evars.
herbelin
2009-12-14
*
Made the side-conditions of lemmas always come last when chaining "apply in"
herbelin
2009-12-13
*
Completion of r12580 (better rendering of dependent rewrite and inversion).
herbelin
2009-12-13
*
Revision 12557 continued (better rendering of dependent rewrite)
herbelin
2009-12-13
*
Updated compatibility for rewriting equality proofs that are dependent
herbelin
2009-12-12
*
Improved the rendering of "dependent rewrite" and hence of "inversion"
herbelin
2009-12-12
*
Restored rewriting of JMeq using JMeq_rect and co when the domains are the same
herbelin
2009-12-03
*
Addendum to revision 12501.
herbelin
2009-11-12
*
Backtracking on the use of automatically generated schemes for
herbelin
2009-11-11
*
A bit of cleaning around name generation + creation of dedicated file namegen.ml
herbelin
2009-11-09
*
Quick fix for restoring a left-to-right rewriting lemma compatible
herbelin
2009-11-09
*
Restructuration of command.ml + generic infrastructure for inductive schemes
herbelin
2009-11-08
*
Remove old compatibility stuff (Tacred.nf)
glondu
2009-10-28
*
Changed the way to support compatibility with previous versions.
herbelin
2009-10-04
*
Fixed a bug in the interaction between dEqThen and inject_at_positions
herbelin
2009-09-27
*
Delay the choice of eliminator in destruct/induction until we know if
herbelin
2009-09-27
*
Delete trailing whitespaces in all *.{v,ml*} files
glondu
2009-09-17
*
Stop trying to search if the relation is declared as a [RewriteRelation]
msozeau
2009-09-09
*
Fix the bug-ridden code used to choose leibniz or generalized
msozeau
2009-09-08
*
Move out JMeq of subst for compatibility (it affects e.g. the
herbelin
2009-08-06
*
Fixed subst failing when a truly heterogeneous JMeq hyp is in the
herbelin
2009-08-04
*
Added "etransitivity".
herbelin
2009-08-03
*
Improved parameterization of Coq:
herbelin
2009-08-02
*
Remove the barely-used/obsolete/undocumented syntax "conditional <tac> rewrite"
letouzey
2009-07-24
*
Reactivation of pattern unification of evars in apply unification, in
herbelin
2009-07-08
*
Jolification : tentative de supprimer les "( evd)" et associés qui
aspiwack
2009-07-07
*
Add new variants of [rewrite] and [autorewrite] which differ in the
msozeau
2009-06-30
*
Reimplementation of leibniz rewrite to control the instantiation of the
msozeau
2009-06-16
*
Some dead code removal + cleanups
letouzey
2009-04-08
*
Fixes to make Ynot compile with the trunk:
msozeau
2009-03-20
*
Cleaning/improving the use of the "in" clause (e.g. "unfold foo in H at 4"
herbelin
2009-03-16
*
Cleaning/uniformizing the interface of tacticals.mli
herbelin
2009-03-14
*
On remplace evar_map par evar_defs (seul evar_defs est désormais exporté
aspiwack
2009-02-19
*
pushed evar reduction in kernel
barras
2009-02-06
[next]