index
:
coq
master
The formal proof system
about
summary
refs
log
tree
commit
diff
log msg
author
committer
range
path:
root
/
tactics
/
coretactics.ml4
Age
Commit message (
Expand
)
Author
2016-03-21
Creating a dedicated ltac/ folder for Hightactics.
Pierre-Marie Pédrot
2016-03-17
Removing the special status of generic arguments defined by Coq itself.
Pierre-Marie Pédrot
2016-03-17
Removing the special status of generic entries defined by Coq itself.
Pierre-Marie Pédrot
2016-03-04
Replacing ad-hoc tactic scopes by generic ones using [create_ltac_quotations].
Pierre-Marie Pédrot
2016-02-29
Moving the "move" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
Moving the "exists" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
Moving the "symmetry" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
Moving the "generalize dependent" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
Moving the "clearbody" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
Moving the "clear" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
Moving the "cofix" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-02-29
Moving the "fix" tactic to TACTIC EXTEND.
Pierre-Marie Pédrot
2016-01-21
Merge branch 'v8.5'
Pierre-Marie Pédrot
2016-01-20
Update copyright headers.
Maxime Dénès
2015-12-27
Tentative API fix for tactic arguments to be fed to tclWITHHOLES.
Pierre-Marie Pédrot
2015-12-25
Moving specialize to Proofview.tactic.
Hugo Herbelin
2015-12-24
Removing auto from the tactic AST.
Pierre-Marie Pédrot
2015-12-21
Changing the toplevel type of the int_or_var generic type to int.
Pierre-Marie Pédrot
2015-12-11
Add tactic native_cast_no_check, analog to vm_cast_no_check.
Maxime Dénès
2015-03-22
Aliasing give_up with admit
Enrico Tassi
2015-02-10
More expressive API for tclWITHHOLES.
Pierre-Marie Pédrot
2015-02-10
Revert "Removing spurious tclWITHHOLES."
Pierre-Marie Pédrot
2015-01-12
Update headers.
Maxime Dénès
2014-12-23
A global [gfail] tactic which works like [fail] except that it fails even if ...
Arnaud Spiwack
2014-12-16
Fixing CAMLP4 compilation.
Pierre-Marie Pédrot
2014-12-12
Extend the syntax of simpl with a delta flag.
Arnaud Spiwack
2014-10-22
Proofview: split [V82] module into [Unsafe] and [V82].
Arnaud Spiwack
2014-09-02
Removing [revert] tactic from the AST.
Pierre-Marie Pédrot
2014-08-31
Getting rid of atomic tactics in Tacenv.
Pierre-Marie Pédrot
2014-08-27
Removing spurious tclWITHHOLES.
Pierre-Marie Pédrot
2014-08-07
Removing simple induction / destruct from the AST.
Pierre-Marie Pédrot
2014-08-07
Instead of relying on a trick to make the constructor tactic parse, put
Pierre-Marie Pédrot
2014-08-07
Removing the "constructor" tactic from the AST.
Pierre-Marie Pédrot
2014-08-06
Removing "intros untils" from the AST.
Pierre-Marie Pédrot
2014-08-01
Removing some tactic compatibility layer.
Pierre-Marie Pédrot
2014-06-17
Removing dead code.
Pierre-Marie Pédrot
2014-06-06
Moving the [split] tactic out of the AST.
Pierre-Marie Pédrot
2014-06-02
Removing symmetry from the atomic tactics.
Pierre-Marie Pédrot
2014-05-22
Moving the "specialize" tactic out of the AST. Also removed an obsolete
Pierre-Marie Pédrot
2014-05-21
Moving left & right tactics out of the AST.
Pierre-Marie Pédrot
2014-05-20
Moving (e)transitivity out of the AST.
Pierre-Marie Pédrot
2014-05-20
Tactics declared through TACTIC EXTEND that are of the form
Pierre-Marie Pédrot
2014-05-20
Tentative to add constr-using primitive tactics without grammar rules.
Pierre-Marie Pédrot
2014-05-16
Moving argument-free tactics out of the AST into a dedicated
Pierre-Marie Pédrot
