index
:
coq
master
the Coq proof assistant
about
summary
refs
log
tree
commit
diff
homepage
log msg
author
committer
range
path:
root
/
tactics
/
tacticals.mli
Commit message (
Expand
)
Author
Age
*
More expressive API for tclWITHHOLES.
Pierre-Marie Pédrot
2015-02-10
*
Removing dead code.
Pierre-Marie Pédrot
2015-02-02
*
Update headers.
Maxime Dénès
2015-01-12
*
Getting rid of Exninfo hacks.
Pierre-Marie Pédrot
2014-12-16
*
Add Ltac syntax for the [tclIFCATCH] primitive.
Arnaud Spiwack
2014-12-12
*
Constructor tactics backtracking is done using [Tacticals.New] rather than [P...
Arnaud Spiwack
2014-12-08
*
Adding locations to tclZEROMSG.
Pierre-Marie Pédrot
2014-11-20
*
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
*
Reorganisation of intropattern code
Hugo Herbelin
2014-08-18
*
Adding a "time" tactical for benchmarking purposes. In case the tactic
Hugo Herbelin
2014-07-13
*
Revert "time tac" (committed by mistake).
Hugo Herbelin
2014-07-07
*
time tac
Hugo Herbelin
2014-07-07
*
Removing dead code.
Pierre-Marie Pédrot
2014-06-17
*
This commit adds full universe polymorphism and fast projections to Coq.
Matthieu Sozeau
2014-05-06
*
Removing dead code, thanks to new OCaml warnings and a bit of scripting.
Pierre-Marie Pédrot
2014-04-23
*
Using the new monad tactic in Inv.
Pierre-Marie Pédrot
2014-04-22
*
Removing tactic compatibility layer from Elim.
Pierre-Marie Pédrot
2014-04-22
*
Simplifying interface of elimination tactics. They used dummy clausenvs, and
Pierre-Marie Pédrot
2014-04-22
*
Removing the Change_evar refiner rule.
Pierre-Marie Pédrot
2014-03-31
*
Removing tactic compatibility layer from Eqdecide.
Pierre-Marie Pédrot
2014-03-27
*
Removing tactic compatibility layer in Equality.
Pierre-Marie Pédrot
2014-03-26
*
Removing Tacmach compatibility layer in Inv.
Pierre-Marie Pédrot
2014-03-26
*
Removing tactic compatibility layer from Inv.
Pierre-Marie Pédrot
2014-03-26
*
Remove many superfluous 'open' indicated by ocamlc -w +33
Pierre Letouzey
2014-03-05
*
Implementation of Ltac's match and match goal fully based on IStream.
aspiwack
2013-11-14
*
Fix ltac's progress tactical: requires progress in each goal.
aspiwack
2013-11-04
*
Update comments.
aspiwack
2013-11-02
*
Adds an experimental exactly_once tactical.
aspiwack
2013-11-02
*
Adds a tactical once.
aspiwack
2013-11-02
*
Added the tactical "tac1 + tac2".
aspiwack
2013-11-02
*
Bases tactics on an IO monad.
aspiwack
2013-11-02
*
Uses Proofview.tclEXTEND more sparingly.
aspiwack
2013-11-02
*
Makes the new Proofview.tactic the basic type of Ltac.
aspiwack
2013-11-02
*
Merging Context and Sign.
ppedrot
2013-04-29
*
Splitting Term into five unrelated interfaces:
ppedrot
2013-04-29
*
Modulification of identifier
ppedrot
2012-12-14
*
Remove some more "open" and dead code thanks to OCaml4 warnings
letouzey
2012-10-02
*
Added a new tactical infoH tac, that displays the names of hypothesis created...
courtieu
2012-10-01
*
Updating headers.
herbelin
2012-08-08
*
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
*
locus.mli for occurrences+clauses, misctypes.mli for various little things
letouzey
2012-05-29
*
info_trivial, info_auto, info_eauto, and debug (trivial|auto)
letouzey
2012-03-30
*
Noise for nothing
pboutill
2012-03-02
*
Rename rawterm.ml into glob_term.ml
glondu
2010-12-23
*
Some dead code removal, thanks to Oug analyzer
letouzey
2010-09-24
*
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
*
Remove the svn-specific $Id$ annotations
letouzey
2010-04-29
[next]