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
*
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
*
Glob_term now mli-only, operations now in Glob_ops
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd
letouzey
2012-05-29
*
Remove the Dp plugin.
gmelquio
2012-04-17
*
Second step of integration of Program:
msozeau
2012-03-14
*
Noise for nothing
pboutill
2012-03-02
*
A "Grab Existential Variables" to transform the unresolved evars at the end o...
aspiwack
2012-02-07
*
Merge subinstances branch by me and Tom Prince.
msozeau
2011-11-17
*
Add type annotations around all calls to Libobject.declare_object
letouzey
2011-11-02
*
A new tactic is_var to check whether a term is a goal/section variable
letouzey
2011-10-07
*
Moving implicit tactic support from Tacinterp to Pfedit and final evar
herbelin
2011-09-26
*
Relaxed the constraint introduced in r14190 that froze the existing
herbelin
2011-06-18
*
- Fix treatment of globality flag for typeclass instance hints (they
msozeau
2011-02-14
*
Rename the "raw" argument extension into "glob"
glondu
2010-12-27
*
More {raw => glob} changes for consistency
glondu
2010-12-24
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Change of nomenclature: rawconstr -> glob_constr
glondu
2010-12-23
*
Add tactic has_evar (#2433)
glondu
2010-12-02
*
Add tactic is_evar (Closes: #2433)
glondu
2010-12-02
[next]