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
*
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
*
Fixing 1177da327 (reorganization of the test for generic selection of
Hugo Herbelin
2014-11-02
*
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
*
Ensuring compatibility when an hypothesis used for destruct is
Hugo Herbelin
2014-10-27
*
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
*
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
*
Proofview: split [V82] module into [Unsafe] and [V82].
Arnaud Spiwack
2014-10-22
*
Remove the deprecated open-constr based refine.
Arnaud Spiwack
2014-10-22
*
Remove duplicate code.
Arnaud Spiwack
2014-10-22
*
Removing re-typecheking from "refine" in no-check mode of the new
Hugo Herbelin
2014-10-20
*
Revert "Essai où assert_style n'est utilisé que si pas visuellement une éq...
Hugo Herbelin
2014-10-17
*
Essai où assert_style n'est utilisé que si pas visuellement une équation;
Hugo Herbelin
2014-10-17
*
Relaxing again the test on types of replacements in tactic change
Hugo Herbelin
2014-10-16
*
In convert_concl/convert_hyp: nf_enter -> enter.
Hugo Herbelin
2014-10-16
*
Refresh to avoid algebraic universes on the right.
Matthieu Sozeau
2014-10-16
*
Goal: remove most of the API (make [Goal.goal] concrete).
Arnaud Spiwack
2014-10-16
*
Proofview.Refine: remove the handle type, and simplify the API.
Arnaud Spiwack
2014-10-16
*
Fix bug #3698: stack overflow due to eta+canonical structures in
Matthieu Sozeau
2014-10-14
*
Fixing "change" and "fold" after convert_hyp/convert_concl moved to
Hugo Herbelin
2014-10-13
*
Add support for deactivating type class inference from induction/destruct.
Hugo Herbelin
2014-10-13
*
Propagating name of goal to main subgoal in cut and conversion tactics.
Hugo Herbelin
2014-10-09
*
A version of convert_concl and convert_hyp in new proof engine.
Hugo Herbelin
2014-10-09
*
Splitting out of auto.ml a file hints.ml dedicated to hints so as to
Hugo Herbelin
2014-10-07
*
Removing debugging information committed by mistake.
Hugo Herbelin
2014-10-07
*
Make tclEFFECTS also update the env in the proof monad
Enrico Tassi
2014-10-06
*
Check compatibility of types in change depending on whether it is a
Hugo Herbelin
2014-10-05
*
Fixing #3657 (check that both sides of a "change with" have the same
Hugo Herbelin
2014-10-03
*
Seeing IntroWildcard as an action intro pattern rather than as a naming pattern
Hugo Herbelin
2014-09-30
*
Add a boolean to indicate the unfolding state of a primitive projection,
Matthieu Sozeau
2014-09-27
*
Changed semantics of induction !id when a clause is given: don't
Hugo Herbelin
2014-09-27
*
Removing the last use of tclSENSITIVE in favour of tclNEWGOALS.
Pierre-Marie Pédrot
2014-09-27
*
Rename eq_constr functions in Evd to not break backward compatibility
Matthieu Sozeau
2014-09-24
*
Make eq_pattern_test/eq_test work up to the equivalence of primitive
Matthieu Sozeau
2014-09-24
*
Be more conservative and keep the use of eq_constr in pretyping/ functions.
Matthieu Sozeau
2014-09-17
*
Fix bug #3593, making constr_eq and progress work up to
Matthieu Sozeau
2014-09-17
*
Fix bug #3633 properly, by delaying the interpetation of constrs in
Matthieu Sozeau
2014-09-17
[next]