index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
tactics.mli
Commit message (
Expand
)
Author
Age
...
*
|
|
Moving specialize to Proofview.tactic.
Hugo Herbelin
2015-12-25
|
/
/
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-11
|
\
|
|
*
Add tactic native_cast_no_check, analog to vm_cast_no_check.
Maxime Dénès
2015-12-11
*
|
Removing redundant versions of generalize.
Hugo Herbelin
2015-12-05
*
|
Merge branch 'v8.5'
Pierre-Marie Pédrot
2015-12-03
|
\
|
|
*
Dead code from August 2014 in apply in.
Hugo Herbelin
2015-12-02
*
|
Monotonizing Tactics.change_arg.
Pierre-Marie Pédrot
2015-10-29
*
|
Type delayed_open_constr is now monotonic.
Pierre-Marie Pédrot
2015-10-19
*
|
Constraining refine to monotonic functions.
Pierre-Marie Pédrot
2015-10-18
|
/
*
Fixing "pose proof (H ...) as H" and "assert (H:=H ...) which were supposed
Hugo Herbelin
2015-09-08
*
Fix #3590 for good this time, by changing the API, change's argument now
Matthieu Sozeau
2015-04-10
*
admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032)
Enrico Tassi
2015-03-11
*
Update headers.
Maxime Dénès
2015-01-12
*
Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic.
Hugo Herbelin
2014-12-07
*
Simplifying code of functional induction.
Hugo Herbelin
2014-11-22
*
Writing intro_replacing in the new monad.
Pierre-Marie Pédrot
2014-11-22
*
Writing Tactics.keep in the new monad.
Pierre-Marie Pédrot
2014-11-21
*
Fixing side bug in db37c9f3f32ae7 delaying interpretation of the
Hugo Herbelin
2014-11-16
*
Removing the unused boolean flag from the move tactic implementation.
Pierre-Marie Pédrot
2014-11-09
*
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
*
This commit introduces changes in induction and destruct.
Hugo Herbelin
2014-10-25
*
Remove the deprecated open-constr based refine.
Arnaud Spiwack
2014-10-22
*
Fixing "change" and "fold" after convert_hyp/convert_concl moved to
Hugo Herbelin
2014-10-13
*
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
*
Fix bug #3633 properly, by delaying the interpetation of constrs in
Matthieu Sozeau
2014-09-17
*
Add a "Hint Mode ref (+ | -)*" hint for setting a global mode
Matthieu Sozeau
2014-09-15
*
Other bugs with "inversion as" (collision between user-provided names and gen...
Hugo Herbelin
2014-09-11
*
Fixing inversion after having fixed intros_replacing
Hugo Herbelin
2014-09-10
*
At last a working clearbody!
Pierre-Marie Pédrot
2014-09-05
*
Revert the two previous commits. I was testing in the wrong branch.
Pierre-Marie Pédrot
2014-09-04
*
Reimplementing the clearbody tactic.
Pierre-Marie Pédrot
2014-09-04
*
Tactics.unify in the new monad.
Pierre-Marie Pédrot
2014-08-23
*
Removing unused parts of the Goal.sensitive monad.
Pierre-Marie Pédrot
2014-08-21
*
Lazy interpretation of patterns so that expressions such as "intros H H'/H"
Hugo Herbelin
2014-08-18
*
Adding a new intro-pattern for "apply in" on the fly. Using syntax
Hugo Herbelin
2014-08-18
*
A few more comments in tactics.mli and hippatern.ml.
Hugo Herbelin
2014-08-18
*
Slight simplification of naming of tactics in equality.ml (hopefully).
Hugo Herbelin
2014-08-18
*
A reorganization of the "assert" tactics (hopefully uniform naming
Hugo Herbelin
2014-08-18
*
Reorganisation of intropattern code
Hugo Herbelin
2014-08-18
*
Reorganization of tactics:
Hugo Herbelin
2014-08-18
*
Experimentally adding an option for automatically erasing an
Hugo Herbelin
2014-08-05
*
Adding a syntax "enough" for the variant of "assert" with the order of
Hugo Herbelin
2014-08-05
*
A new step in the new "standard" naming policy for propositional hypotheses
Hugo Herbelin
2014-08-05
*
Removing some tactic compatibility layer.
Pierre-Marie Pédrot
2014-08-01
*
Fix semantics of change p with c to typecheck c at each specific occurrence o...
Matthieu Sozeau
2014-06-23
*
Passing some tactics to the new monad type.
Pierre-Marie Pédrot
2014-06-12
*
Fixing introduction patterns * and ** when used in a branch so that they do n...
Hugo Herbelin
2014-05-31
*
Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").
Hugo Herbelin
2014-05-31
[prev]
[next]