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
*
Fixing bug #3944.
Pierre-Marie Pédrot
2015-02-16
*
Fixing bug #4016.
Pierre-Marie Pédrot
2015-02-14
*
Univs: fix bug #4031: wrong folding of sigma in change.
Matthieu Sozeau
2015-02-12
*
Fix bug #2775: Correct handling of universes in leminv.
Matthieu Sozeau
2015-02-12
*
Fixing compilation for 3.12.
Pierre-Marie Pédrot
2015-02-12
*
Tentative fix for bug #4027.
Pierre-Marie Pédrot
2015-02-12
*
Missing space in error message
Matěj Grabovský
2015-02-11
*
Fixing #4018 (uncaught exception on non-equality in intros [=]).
Hugo Herbelin
2015-02-10
*
More expressive API for tclWITHHOLES.
Pierre-Marie Pédrot
2015-02-10
*
Revert "Removing spurious tclWITHHOLES."
Pierre-Marie Pédrot
2015-02-10
*
Removing dead code.
Pierre-Marie Pédrot
2015-02-02
*
Removed obsolete option "Legacy Partially Applied Elimination
Hugo Herbelin
2015-01-24
*
Tentative workaround for bug #3798.
Pierre-Marie Pédrot
2015-01-24
*
Univs: proper printing of global and local universe names (only
Matthieu Sozeau
2015-01-17
*
Make native compiler handle universe polymorphic definitions.
Maxime Dénès
2015-01-17
*
Revert "TCs: Properly handle Hint Extern with conclusions of the form _ -> _"
Matthieu Sozeau
2015-01-16
*
Add a (by default deactivated) option to force typeclass resolution to
Matthieu Sozeau
2015-01-15
*
Optionally allow eta-conversion during unification for type classes.
Matthieu Sozeau
2015-01-15
*
TCs: Properly handle Hint Extern with conclusions of the form _ -> _
Matthieu Sozeau
2015-01-13
*
Update headers.
Maxime Dénès
2015-01-12
*
Fixing compilation of penultimate commit d08532d.
Hugo Herbelin
2015-01-08
*
Avoiding introducing yet another convention in naming files.
Hugo Herbelin
2015-01-08
*
Fix setoid rewrite.
Arnaud Spiwack
2015-01-06
*
Fixing #3896 (incorrect sigma given to printer).
Hugo Herbelin
2015-01-03
*
A global [gfail] tactic which works like [fail] except that it fails even if ...
Arnaud Spiwack
2014-12-23
*
Remove compatibility layer from Ltac's [fail].
Arnaud Spiwack
2014-12-23
*
Fix compilation error in some configurations.
Arnaud Spiwack
2014-12-23
*
Add a backtracking version of Ltac's [match].
Arnaud Spiwack
2014-12-19
*
Fixed bad newlines in output for std output and emacs.
Pierre Courtieu
2014-12-18
*
Fixing bug #3796.
Pierre-Marie Pédrot
2014-12-17
*
Fixing CAMLP4 compilation.
Pierre-Marie Pédrot
2014-12-16
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
Add Ltac syntax for the [tclIFCATCH] primitive.
Arnaud Spiwack
2014-12-12
*
Extend the syntax of simpl with a delta flag.
Arnaud Spiwack
2014-12-12
*
In discrimination nets, do not index lambdas if they're part of a beta
Matthieu Sozeau
2014-12-12
*
Tentatively more informative report of failure when inferring
Hugo Herbelin
2014-12-11
*
Fix dummy argument use in guess_elim: there are some cases where X_ind
Matthieu Sozeau
2014-12-10
*
Switch the few remaining iso-latin-1 files to utf8
Pierre Letouzey
2014-12-09
*
This is for documenting and slightly fixing commits 547e97e, c52aea7, 9a34d3e.
Hugo Herbelin
2014-12-08
*
Constructor tactics backtracking is done using [Tacticals.New] rather than [P...
Arnaud Spiwack
2014-12-08
*
Step 4 : atomize_then
Hugo Herbelin
2014-12-07
*
Step 2
Hugo Herbelin
2014-12-07
*
Step 1
Hugo Herbelin
2014-12-07
*
Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.
Hugo Herbelin
2014-12-07
*
Exporting store of goals so that new_evar in convert, intro, etc. can
Hugo Herbelin
2014-12-07
*
For compatibility purpose, when setoid_rewriting a hypothesis, beta-iota
Pierre-Marie Pédrot
2014-12-02
*
More invariants in the code of Rewrite.
Pierre-Marie Pédrot
2014-12-01
*
Continuing a8ad3abc15a2 which actually forgot to ensure freshness in current ...
Hugo Herbelin
2014-11-30
*
Set use_evars_eagerly_in_conv_on_closed_terms in rewrite_unif_flags too.
Hugo Herbelin
2014-11-30
*
Reverting the following block of three commits:
Hugo Herbelin
2014-11-27
[next]