index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
tactics.ml
Commit message (
Expand
)
Author
Age
*
- Cleaning phase of the interfaces of libnames.ml and nametab.ml
herbelin
2009-08-06
*
- Add more precise error localisation when one of the application fails
herbelin
2009-08-04
*
Added "etransitivity".
herbelin
2009-08-03
*
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
*
Reimplementation of leibniz rewrite to control the instantiation of the
msozeau
2009-06-16
*
- Added two new introduction patterns with the following temptative syntaxes:
herbelin
2009-06-07
*
Fixing bug 2110 (tactic "refine" was calling (co)mutual_fix with index 0
herbelin
2009-06-06
*
Minor unification changes:
msozeau
2009-05-18
*
- Allowing multiple calls to tactic fix with automatic generation of
herbelin
2009-05-17
*
Backporting 12080 (fixing bug #2091 on bad rollback in the "where"
herbelin
2009-04-24
*
Fix premature optimisation in dependent induction: even variable args need
msozeau
2009-04-10
*
Fix auto so that Extern tactics associated to no patterns can apply to
msozeau
2009-03-31
*
Compromise wrt introduction-names compatibility issue after addition
herbelin
2009-03-22
*
Uniformizing Tacticals, continued (allClauses -> allHypsAndConcl)
herbelin
2009-03-17
*
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
*
Add support for dependent "destruct" over terms in dependent types.
herbelin
2009-02-23
*
On remplace evar_map par evar_defs (seul evar_defs est désormais exporté
aspiwack
2009-02-19
*
Fix [apply_in] which short-circuited resolution of evars in a custom
msozeau
2009-02-16
*
pushed evar reduction in kernel
barras
2009-02-06
*
Report r11631 from 8.2 and handle non-dependent goals better in
msozeau
2009-02-04
*
Fixed bugs #2001 (search_guard was overwriting the guard index given
herbelin
2009-01-04
*
Fixed two problems:
herbelin
2009-01-03
*
- Temptative change to notations like "as [|n H]_eqn" or "as [|n H]_eqn:H",
herbelin
2009-01-02
*
Moved parts of Sign to Term. Unified some names (e.g. decomp_n_prod ->
herbelin
2008-12-31
*
- Added support for subterm matching in SearchAbout.
herbelin
2008-12-29
*
- Another bug in get_sort_family_of (sort-polymorphism of constants and
herbelin
2008-12-28
*
- Extracted from the tactic "now" an experimental tactic "easy" for small
herbelin
2008-12-26
*
- Fixed cutrewrite bug #2021 introduced in commit 11662 (as a side
herbelin
2008-12-18
*
Finish fix for the treatment of [inverse] in [setoid_rewrite], making a
msozeau
2008-12-16
*
Fixed in bug in previous 11662 (incorrect with_evars flag in descend_conjunct...
herbelin
2008-12-12
*
About "apply in":
herbelin
2008-12-09
*
closed bug 1898: fold x in x; added a reordering primitive tactic
barras
2008-11-26
*
- Fixed minor bug #1994 in the tactic chapter of the manual [doc]
herbelin
2008-11-22
*
Port [rewrite] tactics to open terms. Currently no check that evars
msozeau
2008-11-05
*
Adaptation du vieil appel à "apply" sur lemme de symétrie au cas où
herbelin
2008-10-29
*
- Fixed many "Theorem with" bugs.
herbelin
2008-10-27
*
Fixes and refinements regarding occurrence selection:
herbelin
2008-10-26
*
Backtrack sur commit 11467 (tentative d'optimisation meta_instance qui
herbelin
2008-10-26
*
Fix bug #1977 by allowing the [apply] variants to take an [open_constr]
msozeau
2008-10-23
*
Optimisation de clenv.ml pour que meta_instance ne soit pas appelé
herbelin
2008-10-18
*
Various little improvements:
msozeau
2008-09-25
*
Add a type argument to letin_tac instead of using casts and recomputing
msozeau
2008-09-12
*
Fixes in dependent induction tactic, putting things in better order for
msozeau
2008-09-11
*
Fix bug #1935, reworking the reflexivity, symmetry... tactics to use
msozeau
2008-09-03
*
Fixes in dependent induction tactic to keep names, allow giving
msozeau
2008-08-21
*
Évolutions diverses et variées.
herbelin
2008-08-04
*
Fixes in generalize_eqs/dependent induction to allow the user to specify
msozeau
2008-07-28
*
New tactics [conv] to test convertibility (actually, unification) of two
msozeau
2008-07-22
[next]