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
...
*
Replugging hints in rewriting strategies.
Pierre-Marie Pédrot
2014-11-10
*
Fixing wrongly used tclWITHHOLES in named tactics (continuation of 9fa45b3).
Pierre-Marie Pédrot
2014-11-10
*
Fixing bug #3803.
Pierre-Marie Pédrot
2014-11-09
*
Removing the unused boolean flag from the move tactic implementation.
Pierre-Marie Pédrot
2014-11-09
*
Removing a unused boolean in the TacMove node of tacexpr AST.
Pierre-Marie Pédrot
2014-11-09
*
new: Optimize Proof, Optimize Heap
Enrico Tassi
2014-11-09
*
Follow up to experimental eager evar unification in bcba6d1bc9:
Hugo Herbelin
2014-11-08
*
Compatibility with 8.4 in the heuristic used to build the induction
Hugo Herbelin
2014-11-08
*
Granting #3717 (more informative error message on missing arguments for funct...
Hugo Herbelin
2014-11-07
*
Fixing #3562 ("as" in "destruct" expects either a disjunctive
Hugo Herbelin
2014-11-07
*
Removing the legacy intro tactic code.
Pierre-Marie Pédrot
2014-11-07
*
Print [rename] tactic properly in info trace.
Arnaud Spiwack
2014-11-07
*
Restoring clear_flag (thanks a lot to jonikelee to notice it).
Hugo Herbelin
2014-11-06
*
Optimizing when to clear generalized hypotheses in destruct.
Hugo Herbelin
2014-11-06
*
Dependency bug in using eqn for destruct.
Hugo Herbelin
2014-11-06
*
Writing the raw introduction tactic in the new monad.
Pierre-Marie Pédrot
2014-11-05
*
Writing rename_hyps in the new monad.
Pierre-Marie Pédrot
2014-11-03
*
Subtle swap of lines to preserve VarInstance src field before checking
Hugo Herbelin
2014-11-03
*
Fix to 844431761 on improving elimination with indices, getting rid of
Hugo Herbelin
2014-11-03
*
Saving some nf_evars in the code of destruct/induction.
Hugo Herbelin
2014-11-02
*
Improving elimination with indices, getting rid of intrusive residual
Hugo Herbelin
2014-11-02
*
Some reorganization of the code for destruct/induction:
Hugo Herbelin
2014-11-02
*
Plural and singular forms in error messages.
Hugo Herbelin
2014-11-02
*
Fixing 1177da327 (reorganization of the test for generic selection of
Hugo Herbelin
2014-11-02
*
Info: the warning message of the defunct [info] tactic now points to the [Inf...
Arnaud Spiwack
2014-11-01
*
Info: print name of calls to Ltac constants ([TacCall]).
Arnaud Spiwack
2014-11-01
*
Info: tactic notations (TacAlias) print their names.
Arnaud Spiwack
2014-11-01
*
Info: Tactics coming from [TACTIC EXTEND] print their names.
Arnaud Spiwack
2014-11-01
*
Info: print the name of atomic tactics.
Arnaud Spiwack
2014-11-01
*
Info: Ltac's idtac logs its message in the info trace.
Arnaud Spiwack
2014-11-01
*
Reorganization of the test for generic selection of occurrences in
Hugo Herbelin
2014-10-31
*
Enlarge the cases where the like first selection is used in destruct.
Hugo Herbelin
2014-10-31
*
Avoid "destruct H" to apply on H itself when H is a section variable.
Hugo Herbelin
2014-10-31
*
Cleaning and documenting Clenv.make_evar_clause
Pierre-Marie Pédrot
2014-10-27
*
Removing the last Evd.diff from Hints.
Pierre-Marie Pédrot
2014-10-27
*
Making destruct on idents with maximal implicit arguments working, by
Hugo Herbelin
2014-10-27
*
Ensuring compatibility when an hypothesis used for destruct is
Hugo Herbelin
2014-10-27
*
Fixing evars lost in interpretation of eliminator of destruct.
Hugo Herbelin
2014-10-27
*
Preventing potential evar leak in Rewrite.
Pierre-Marie Pédrot
2014-10-26
*
Fixing destruct/induction with a using clause on a non-inductive type,
Hugo Herbelin
2014-10-26
*
Dead code + typo.
Hugo Herbelin
2014-10-26
*
This commit introduces changes in induction and destruct.
Hugo Herbelin
2014-10-25
*
Change reduction_of_red_expr to return an e_reduction_function returning
Matthieu Sozeau
2014-10-24
*
Apparently, the former refine was simplifying in hypotheses too.
Hugo Herbelin
2014-10-24
*
Addressing report #3279 (inconsistency of behavior of the -> and <-
Hugo Herbelin
2014-10-24
*
Specializing tclBREAK so that it can choose the return exception in case
Pierre-Marie Pédrot
2014-10-22
*
Refine tactic: simplify the conclusion only at the end of the tactic.
Arnaud Spiwack
2014-10-22
*
Remove an unnecessary use of [Proofview.Unsafe.tclEVARS] in [convert_concl].
Arnaud Spiwack
2014-10-22
*
Split [Proofview] into a file where the basic operations on the state are def...
Arnaud Spiwack
2014-10-22
*
Make names in [Proofview_monad] more uniform.
Arnaud Spiwack
2014-10-22
[prev]
[next]