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
*
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
*
Moving the "specialize" tactic out of the AST. Also removed an obsolete
Pierre-Marie Pédrot
2014-05-22
*
Code cleaning & factorizing functions in Equality.
Pierre-Marie Pédrot
2014-05-09
*
Encapsulating some clausenv uses. This simplifies the control flow of some
Pierre-Marie Pédrot
2014-05-08
*
Isolating a function "make_abstraction", new name of "letin_abstract",
Hugo Herbelin
2014-05-08
*
Renaming new_induct -> induction; new_destruct -> destruct.
Hugo Herbelin
2014-05-08
*
- Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...
Matthieu Sozeau
2014-05-08
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Rewriting [lapply] tactic in the new monad.
Pierre-Marie Pédrot
2014-04-27
*
Writing tclABSTRACT in the new monad. In particular the unsafe status is now
Pierre-Marie Pédrot
2014-04-24
*
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Pierre-Marie Pédrot
2014-04-23
*
Removing the Change_evar refiner rule.
Pierre-Marie Pédrot
2014-03-31
*
Removing dead code in Tactics.
Pierre-Marie Pédrot
2014-03-31
*
Define Tactics.bring_hyps in the new monad.
Pierre-Marie Pédrot
2014-03-28
*
Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.
Pierre-Marie Pédrot
2014-03-26
*
Removing Tacmach compatibility layer in Inv.
Pierre-Marie Pédrot
2014-03-26
*
Moving some tactic code to the new engine.
Pierre-Marie Pédrot
2014-03-26
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Writing [cut] tactic using the new monad.
Pierre-Marie Pédrot
2013-12-02
*
Remove the Hiddentac module.
Arnaud Spiwack
2013-11-25
*
Porting Tactics.assumption to the new engine.
ppedrot
2013-11-08
*
A whole new implemenation of the refine tactic.
aspiwack
2013-11-02
*
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2013-11-02
*
State Transaction Machine
gareuselesinge
2013-08-08
*
Revising r16550 about providing intro patterns for applying injection:
herbelin
2013-07-09
*
Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as an
herbelin
2013-06-02
*
Use the Hook module here and there.
ppedrot
2013-05-12
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Modulification of name
ppedrot
2012-12-18
*
Modulification of identifier
ppedrot
2012-12-14
*
Updating headers.
herbelin
2012-08-08
*
induction/destruct : nicer syntax for generating equations (solves #2741)
letouzey
2012-07-09
*
Added an indirection with respect to Loc in Compat. As many [open Compat]
ppedrot
2012-06-22
*
remove many excessive open Util & Errors in mli's
letouzey
2012-05-29
*
global_reference migrated from Libnames to new Globnames, less deps in gramma...
letouzey
2012-05-29
*
New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr
letouzey
2012-05-29
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
Noise for nothing
pboutill
2012-03-02
*
Added support for referring to subterms of the goal by pattern.
herbelin
2011-09-26
*
Exported tactic intro_then
herbelin
2011-08-10
*
Use "subst_one" instead of "multi_rewrite" to implement intro-patterns -> and...
herbelin
2011-07-16
*
Moved allow_K to a unification flag
herbelin
2011-06-10
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Updated all headers for 8.3 and trunk
herbelin
2010-07-24
*
New script dev/tools/change-header to automatically update Coq files headers.
herbelin
2010-06-22
[next]