aboutsummaryrefslogtreecommitdiffhomepage
path: root/tactics/tacintern.ml
Commit message (Expand)AuthorAge
* This commit introduces changes in induction and destruct.Gravatar Hugo Herbelin2014-10-25
* Splitting out of auto.ml a file hints.ml dedicated to hints so as toGravatar Hugo Herbelin2014-10-07
* Seeing IntroWildcard as an action intro pattern rather than as a naming patternGravatar Hugo Herbelin2014-09-30
* Using an or_var rather than the hack with loc for coding a pure identGravatar Hugo Herbelin2014-09-24
* Removing the XML plugin.Gravatar Pierre-Marie Pédrot2014-09-08
* Silence an ocaml warning.Gravatar Arnaud Spiwack2014-09-05
* Useless hooks in Tacintern.Gravatar Pierre-Marie Pédrot2014-09-03
* Code factorization in Tacintern.Gravatar Pierre-Marie Pédrot2014-09-03
* Removing [revert] tactic from the AST.Gravatar Pierre-Marie Pédrot2014-09-02
* Moving the decompose tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-09-01
* Code cleaning in Tacintern.Gravatar Pierre-Marie Pédrot2014-09-01
* Getting rid of atomic tactics in Tacenv.Gravatar Pierre-Marie Pédrot2014-08-31
* Type-safe version of genarg list / pair / opt functions.Gravatar Pierre-Marie Pédrot2014-08-29
* Adding a new intro-pattern for "apply in" on the fly. Using syntaxGravatar Hugo Herbelin2014-08-18
* Reorganisation of intropattern codeGravatar Hugo Herbelin2014-08-18
* Moving the TacAlias node out of atomic tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Moving the TacExtend node from atomic to plain tactics.Gravatar Pierre-Marie Pédrot2014-08-18
* Removing simple induction / destruct from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
* Instead of relying on a trick to make the constructor tactic parse, putGravatar Pierre-Marie Pédrot2014-08-07
* Removing the "constructor" tactic from the AST.Gravatar Pierre-Marie Pédrot2014-08-07
* Revert the change in Constrintern introduced by "Add a type of untyped term t...Gravatar Arnaud Spiwack2014-08-06
* Removing "intros untils" from the AST.Gravatar Pierre-Marie Pédrot2014-08-06
* 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
* Better struture for Ltac internalization environments in Constrintern.Gravatar Pierre-Marie Pédrot2014-08-02
* New tactical [> t1…tn] to apply tactics t1…tn to the corresponding goal.Gravatar Arnaud Spiwack2014-08-01
* Add [numgoal] to Ltac.Gravatar Arnaud Spiwack2014-08-01
* Untyped terms in tactic: function [type_term c] to give a typed version of [c].Gravatar Arnaud Spiwack2014-07-29
* Add a type of untyped term to Ltac's value.Gravatar Arnaud Spiwack2014-07-29
* Removing dead code relative to or_metaid.Gravatar Pierre-Marie Pédrot2014-07-25
* Distinguish tactics t1;t2 and t1;[t2..].Gravatar Arnaud Spiwack2014-07-24
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
* Revert "time tac" (committed by mistake).Gravatar Hugo Herbelin2014-07-07
* time tacGravatar Hugo Herbelin2014-07-07
* Removing dead code.Gravatar Pierre-Marie Pédrot2014-06-17
* Moving the [split] tactic out of the AST.Gravatar Pierre-Marie Pédrot2014-06-06
* Moving the "specialize" tactic out of the AST. Also removed an obsoleteGravatar Pierre-Marie Pédrot2014-05-22
* Removing useless use of metaids in tactic AST.Gravatar Pierre-Marie Pédrot2014-05-22
* Removing decompose record / sum from the tactic AST.Gravatar Pierre-Marie Pédrot2014-05-21
* Moving left & right tactics out of the AST.Gravatar Pierre-Marie Pédrot2014-05-21
* Moving (e)transitivity out of the AST.Gravatar Pierre-Marie Pédrot2014-05-20
* Tentative to add constr-using primitive tactics without grammar rules.Gravatar Pierre-Marie Pédrot2014-05-20
* Moving argument-free tactics out of the AST into a dedicatedGravatar Pierre-Marie Pédrot2014-05-16
* This commit adds full universe polymorphism and fast projections to Coq.Gravatar Matthieu Sozeau2014-05-06
* Closing bug #3260Gravatar Julien Forest2014-04-14
* Remove many superfluous 'open' indicated by ocamlc -w +33Gravatar Pierre Letouzey2014-03-05
* Removing the useless pattern ident genarg.Gravatar Pierre-Marie Pédrot2013-12-19
* Removing the need of evarmaps in constr internalization.Gravatar Pierre-Marie Pédrot2013-12-17
* Removing RefArgType generic argument.Gravatar Pierre-Marie Pédrot2013-12-01
* Getting rid of casted_open_constr. It was only used by theGravatar Pierre-Marie Pédrot2013-11-30
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 05:33:23 +0000