aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tactics.mli
Commit message (Expand)AuthorAge
* Tactics.unify in the new monad.Gravatar Pierre-Marie Pédrot2014-08-23
* Removing unused parts of the Goal.sensitive monad.Gravatar Pierre-Marie Pédrot2014-08-21
* 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
* A few more comments in tactics.mli and hippatern.ml.Gravatar Hugo Herbelin2014-08-18
* Slight simplification of naming of tactics in equality.ml (hopefully).Gravatar Hugo Herbelin2014-08-18
* A reorganization of the "assert" tactics (hopefully uniform namingGravatar Hugo Herbelin2014-08-18
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
* Reorganization of tactics:Gravatar Hugo Herbelin2014-08-18
* Experimentally adding an option for automatically erasing anGravatar Hugo Herbelin2014-08-05
* Adding a syntax "enough" for the variant of "assert" with the order ofGravatar Hugo Herbelin2014-08-05
* A new step in the new "standard" naming policy for propositional hypothesesGravatar Hugo Herbelin2014-08-05
* Removing some tactic compatibility layer.Gravatar Pierre-Marie Pédrot2014-08-01
* Fix semantics of change p with c to typecheck c at each specific occurrence o...Gravatar Matthieu Sozeau2014-06-23
* Passing some tactics to the new monad type.Gravatar Pierre-Marie Pédrot2014-06-12
* Fixing introduction patterns * and ** when used in a branch so that they do n...Gravatar Hugo Herbelin2014-05-31
* Upgrade Matthieu's new_revert as the "revert" (a "unit tactic").Gravatar Hugo Herbelin2014-05-31
* Moving the "specialize" tactic out of the AST. Also removed an obsoleteGravatar Pierre-Marie Pédrot2014-05-22
* Code cleaning & factorizing functions in Equality.Gravatar Pierre-Marie Pédrot2014-05-09
* Encapsulating some clausenv uses. This simplifies the control flow of someGravatar Pierre-Marie Pédrot2014-05-08
* Isolating a function "make_abstraction", new name of "letin_abstract",Gravatar Hugo Herbelin2014-05-08
* Renaming new_induct -> induction; new_destruct -> destruct.Gravatar Hugo Herbelin2014-05-08
* - Add a primitive tclEVARUNIVERSECONTEXT to reset the universe context of an ...Gravatar Matthieu Sozeau2014-05-08
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Rewriting [lapply] tactic in the new monad.Gravatar Pierre-Marie Pédrot2014-04-27
* Writing tclABSTRACT in the new monad. In particular the unsafe status is nowGravatar Pierre-Marie Pédrot2014-04-24
* Removing dead code, thanks to new OCaml warnings and a bit of scripting.Gravatar Pierre-Marie Pédrot2014-04-23
* Removing the Change_evar refiner rule.Gravatar Pierre-Marie Pédrot2014-03-31
* Removing dead code in Tactics.Gravatar Pierre-Marie Pédrot2014-03-31
* Define Tactics.bring_hyps in the new monad.Gravatar Pierre-Marie Pédrot2014-03-28
* Adding a tclEFFECTS primitive allowing to push STM side-effects in tactics.Gravatar Pierre-Marie Pédrot2014-03-26
* Removing Tacmach compatibility layer in Inv.Gravatar Pierre-Marie Pédrot2014-03-26
* Moving some tactic code to the new engine.Gravatar Pierre-Marie Pédrot2014-03-26
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Writing [cut] tactic using the new monad.Gravatar Pierre-Marie Pédrot2013-12-02
* Remove the Hiddentac module.Gravatar Arnaud Spiwack2013-11-25
* Porting Tactics.assumption to the new engine.Gravatar ppedrot2013-11-08
* A whole new implemenation of the refine tactic.Gravatar aspiwack2013-11-02
* Makes the new Proofview.tactic the basic type of Ltac.Gravatar aspiwack2013-11-02
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Revising r16550 about providing intro patterns for applying injection:Gravatar herbelin2013-07-09
* Now interpreting introduction patterns [x1 .. xn] and (x1,..,xn) as anGravatar herbelin2013-06-02
* Use the Hook module here and there.Gravatar ppedrot2013-05-12
* Merging Context and Sign.Gravatar ppedrot2013-04-29
* Splitting Term into five unrelated interfaces:Gravatar ppedrot2013-04-29
* Modulification of nameGravatar ppedrot2012-12-18
* Modulification of identifierGravatar ppedrot2012-12-14
* Updating headers.Gravatar herbelin2012-08-08
* induction/destruct : nicer syntax for generating equations (solves #2741)Gravatar letouzey2012-07-09
* Added an indirection with respect to Loc in Compat. As many [open Compat]Gravatar ppedrot2012-06-22
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 22:39:58 +0000