aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacticals.ml
Commit message (Expand)AuthorAge
* Update copyright headers.Gravatar Maxime Dénès2016-01-20
* More optimizations of [Clenv.clenv_fchain].Gravatar Pierre-Marie Pédrot2015-11-17
* Univs: fix many evar_map initializations and leaks.Gravatar Matthieu Sozeau2015-10-02
* Safer typing primitives.Gravatar Pierre-Marie Pédrot2015-05-13
* Remove almost all the uses of string concatenation when building error messages.Gravatar Guillaume Melquiond2015-04-23
* Using tclZEROMSG instead of tclZERO in several places.Gravatar Pierre-Marie Pédrot2015-04-23
* More expressive API for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2015-02-10
* Removing dead code.Gravatar Pierre-Marie Pédrot2015-02-02
* Update headers.Gravatar Maxime Dénès2015-01-12
* Fixing #3896 (incorrect sigma given to printer).Gravatar Hugo Herbelin2015-01-03
* Getting rid of Exninfo hacks.Gravatar Pierre-Marie Pédrot2014-12-16
* Add Ltac syntax for the [tclIFCATCH] primitive.Gravatar Arnaud Spiwack2014-12-12
* Tentatively more informative report of failure when inferringGravatar Hugo Herbelin2014-12-11
* Constructor tactics backtracking is done using [Tacticals.New] rather than [P...Gravatar Arnaud Spiwack2014-12-08
* Adding locations to tclZEROMSG.Gravatar Pierre-Marie Pédrot2014-11-20
* Plural and singular forms in error messages.Gravatar Hugo Herbelin2014-11-02
* Proofview: split [V82] module into [Unsafe] and [V82].Gravatar Arnaud Spiwack2014-10-22
* Display number of available goals in "incorrect number of goals" error message.Gravatar Arnaud Spiwack2014-09-08
* Renaming goal-entering functions.Gravatar Pierre-Marie Pédrot2014-09-06
* Simplification of the tclCHECKINTERRUPT tactic.Gravatar Pierre-Marie Pédrot2014-08-28
* Lazy interpretation of patterns so that expressions such as "intros H H'/H"Gravatar Hugo Herbelin2014-08-18
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* Improving error message when applying rewrite to an expression which is not a...Gravatar Hugo Herbelin2014-08-18
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
* More self-contained code for tclWITHHOLES.Gravatar Pierre-Marie Pédrot2014-08-15
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
* check_for_interrupt: better (but slower) in threading modeGravatar Enrico Tassi2014-07-10
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
* time tacGravatar Hugo Herbelin2014-07-07
* Clenvtac.clenv_refine in the new monad. Not satisfactory though, because itGravatar Pierre-Marie Pédrot2014-06-24
* Removing opens to Clenvtac to track its use more easily.Gravatar Pierre-Marie Pédrot2014-06-23
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Using the new monad tactic in Inv.Gravatar Pierre-Marie Pédrot2014-04-22
* Removing tactic compatibility layer from Elim.Gravatar Pierre-Marie Pédrot2014-04-22
* Small code cleaning in Tacticals.Gravatar Pierre-Marie Pédrot2014-04-22
* Simplifying interface of elimination tactics. They used dummy clausenvs, andGravatar Pierre-Marie Pédrot2014-04-22
* Removing the Change_evar refiner rule.Gravatar Pierre-Marie Pédrot2014-03-31
* Removing tactic compatibility layer in Equality.Gravatar Pierre-Marie Pédrot2014-03-26
* Removing Tacmach compatibility layer in Inv.Gravatar Pierre-Marie Pédrot2014-03-26
* Removing tactic compatibility layer from Inv.Gravatar Pierre-Marie Pédrot2014-03-26
* Using non-normalized goals in tactic interpretation.Gravatar Pierre-Marie Pédrot2014-03-19
* Useless tactic bindings in Tacticals.Gravatar Pierre-Marie Pédrot2014-03-07
* Proofview.Notations: Now that (>>=) is free, use it for tclBIND.Gravatar Arnaud Spiwack2014-02-27
* Fix Tacticals.New.tclREPEAT_MAiN: does not fail badly when every goal was sol...Gravatar aspiwack2013-11-04
* Fix ltac's progress tactical: requires progress in each goal.Gravatar aspiwack2013-11-04
* Fix the tactical ; [ … ] : the "incorrect number of goal" error was not cau...Gravatar aspiwack2013-11-04
* The repeat tactic now honors failure levels in ltac.Gravatar aspiwack2013-11-02
* Tacticals.New.tclWITHHOLES: clean up.Gravatar aspiwack2013-11-02
* Adds an experimental exactly_once tactical.Gravatar aspiwack2013-11-02
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 07:59:32 +0000