index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
extratactics.ml4
Commit message (
Expand
)
Author
Age
...
*
Removing the Change_evar refiner rule.
Pierre-Marie Pédrot
2014-03-31
*
Moving some tactic code to the new engine.
Pierre-Marie Pédrot
2014-03-26
*
Proofview.Notations: Now that (>>=) is free, use it for tclBIND.
Arnaud Spiwack
2014-02-27
*
Get rid of the enterl/glist API for Proofview.Goal.
Arnaud Spiwack
2014-02-27
*
Exporting the full pretyper options in Goal.constr_of_raw.
Pierre-Marie Pédrot
2014-01-10
*
Ensuring the right parsing of glob arguments, used by refine
Pierre-Marie Pédrot
2013-12-01
*
Fixing ltac constr variable handling in refine.
Pierre-Marie Pédrot
2013-11-30
*
Getting rid of casted_open_constr. It was only used by the
Pierre-Marie Pédrot
2013-11-30
*
Adding generic solvers to term holes. For now, no resolution mechanism nor
Pierre-Marie Pédrot
2013-11-27
*
Remove the Hiddentac module.
Arnaud Spiwack
2013-11-25
*
Doc: solve the bad interaction between Declare Implicit Tactic and refine.
aspiwack
2013-11-02
*
Refine: Tactics.New.refine does beta-reduction.
aspiwack
2013-11-02
*
Adds a tactic give_up.
aspiwack
2013-11-02
*
A tactic shelve_unifiable.
aspiwack
2013-11-02
*
Adds a shelve tactic.
aspiwack
2013-11-02
*
Refine does beta-reductions.
aspiwack
2013-11-02
*
Less use of the list-based interface for goal-bound tactics.
aspiwack
2013-11-02
*
Tachmach.New is now in Proofview.Goal.enter style.
aspiwack
2013-11-02
*
More Proofview.Goal.enter.
aspiwack
2013-11-02
*
Clean up a warning.
aspiwack
2013-11-02
*
The tactic [admit] exits with the "unsafe" status.
aspiwack
2013-11-02
*
A whole new implemenation of the refine tactic.
aspiwack
2013-11-02
*
Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations.
aspiwack
2013-11-02
*
Getting rid of Goal.here, and all the related exceptions and combinators.
aspiwack
2013-11-02
*
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2013-11-02
*
Moving side effects into evar_map. There was no reason to keep another
ppedrot
2013-10-05
*
Vernac classification streamlined (handles VERNAC EXTEND)
gareuselesinge
2013-08-08
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Start documenting new [rewrite_strat] tactic that applies rewriting
msozeau
2013-06-04
*
Making the behavior of "injection ... as ..." more natural:
herbelin
2013-06-02
*
Granting wish #3014:
ppedrot
2013-05-12
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
code simplifications concerning Summary
letouzey
2013-04-22
*
Restrict (try...with...) to avoid catching critical exn (part 13)
letouzey
2013-03-13
*
Removing Exc_located and using the new exception enrichement
ppedrot
2013-02-18
*
Uniformization of the "anomaly" command.
ppedrot
2013-01-28
*
Modulification of identifier
ppedrot
2012-12-14
*
Finish patch for Hint Resolve, stopping to generate new constant names for
msozeau
2012-12-08
*
Monomorphization (tactics)
ppedrot
2012-11-25
*
Change Hint Resolve, Immediate to take a global reference as argument
msozeau
2012-10-26
*
Continue killing hidden tactics : no more generated h_xxx
letouzey
2012-10-15
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
As r15801: putting everything from Util.array_* to CArray.*.
ppedrot
2012-09-14
*
Updating headers.
herbelin
2012-08-08
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
Getting rid of Pp.msgnl and Pp.message.
ppedrot
2012-06-01
*
tactic is_fix, akin to is_evar, is_hyp, is_ ... family
pboutill
2012-05-31
*
Getting rid of Pp.msg
ppedrot
2012-05-30
*
place all files specific to camlp4 syntax extensions in grammar/
letouzey
2012-05-29
*
Basic stuff about constr_expr migrated from topconstr to constrexpr_ops
letouzey
2012-05-29
[prev]
[next]