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
...
*
A fine-grain control of inlining at functor application via priority levels
letouzey
2011-01-31
*
Remove the "Boxed" syntaxes and the const_entry_boxed field
letouzey
2011-01-28
*
Add [Typeclasses Debug] option that respects backtracking, solve
msozeau
2011-01-11
*
Rename the "raw" argument extension into "glob"
glondu
2010-12-27
*
ARGUMENT EXTEND: forbid TYPED simultaneously with {RAW,GLOB}_TYPED
glondu
2010-12-25
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
tactics/eqdecide.ml4: avoid a useless argument in decideEquality
glondu
2010-12-24
*
Remove the two-argument variant of "decide equality"
glondu
2010-12-23
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Evar-related speed-up and clarifications in Class_tactics and Rewrite
letouzey
2010-12-15
*
Misc improvements about evar_map
letouzey
2010-12-15
*
Class_tactics: avoid an Evd.fold taking ages in contrib ProjectiveGeometry
letouzey
2010-12-13
*
Add tactic has_evar (#2433)
glondu
2010-12-02
*
Add tactic is_evar (Closes: #2433)
glondu
2010-12-02
*
Delayed the evar normalization in error messages to the last minute
herbelin
2010-11-07
*
An experimental support for open constrs in hints and in "using"
herbelin
2010-10-31
*
Cleaning the use of parentheses around evd and evdref (cosmetic commit).
herbelin
2010-10-31
*
Slight code cleaning in auto.ml (made code of make_exact_entry and
herbelin
2010-10-31
*
correction of bug #2414 (report of r 13586)
jforest
2010-10-27
*
Automatically translate hints of the form "c _ ... _" into "c". Besides
herbelin
2010-10-23
*
Two [Evd.fold] turned into [Evd.fold_undefined].
aspiwack
2010-10-04
*
Simplify tactic(_)-bound arguments in TACTIC EXTEND rules
glondu
2010-09-30
*
Remove some occurrences of "open Termops"
glondu
2010-09-28
*
Remove "init" label from Termops.it_mk* specialized functions
glondu
2010-09-28
*
Fix bug in implementation of setoid rewriting under cases and
msozeau
2010-09-27
*
Solving bug #2212 (unification under tuples now not allowed for
herbelin
2010-09-24
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
Added eta-expansion in kernel, type inference and tactic unification,
herbelin
2010-09-20
*
Fixing bug #2360 (descend_in_conjunctions built ill-typed terms). Shouldn't we
herbelin
2010-09-19
*
Reverting partial fix for #2335 committed by mistake in r13435. Sorry.
herbelin
2010-09-19
*
Patch solving the bug but leaving open design choices
herbelin
2010-09-19
*
Fixed a problem introduced in r12607 after pattern_of_constr served
herbelin
2010-09-17
*
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
*
Improving a few error messages in Ltac interpretation
herbelin
2010-09-11
*
* removed declare_constant and declare_internal_constant
vsiles
2010-09-02
*
Improved printing of Unfoldable constants in hints databases (used
herbelin
2010-09-02
*
Export printing functions for extra arguments. Maybe there's a way to
msozeau
2010-08-03
*
Capitulation wrt "change pat with term": instead of solving the
herbelin
2010-07-30
*
Fix bug #2209, don't use the fragile argument name "y" to pass the
msozeau
2010-07-28
*
oops. commited files I shouldn't have. reverting on r13341
barras
2010-07-28
*
ported r13340 to trunk
barras
2010-07-28
*
Minor fixes:
msozeau
2010-07-27
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
Cleaned a bit the grammar and terminology for binders (see dev/doc/changes.txt).
herbelin
2010-07-22
*
Adding the destauto tactic, that reduces match by destructing matched
courtieu
2010-07-22
*
Fix for bug #2350 was really too quick. Here is a version that works better.
herbelin
2010-07-21
*
Quick fix for bug #2350 (ensuring enough "red" when refine calls fix tactic).
herbelin
2010-07-21
*
Reverted 13293 commited mistakenly. Sorry for the noise.
herbelin
2010-07-18
[prev]
[next]