| Commit message (Expand) | Author | Age |
... | |
* | Adding a syntax "enough" for the variant of "assert" with the order of | Hugo Herbelin | 2014-08-05 |
* | Properly declare uconstr as an argument for TACTIC EXTEND. | Arnaud Spiwack | 2014-08-05 |
* | Moving the [split] tactic out of the AST. | Pierre-Marie Pédrot | 2014-06-06 |
* | Removing symmetry from the atomic tactics. | Pierre-Marie Pédrot | 2014-06-02 |
* | Fixing commit 9cef834. The parsing rules were generating an empty list, | Pierre-Marie Pédrot | 2014-05-26 |
* | Complying with reference manual for the syntax of exists/eexists, i.e. | Hugo Herbelin | 2014-05-24 |
* | Moving the "specialize" tactic out of the AST. Also removed an obsolete | Pierre-Marie Pédrot | 2014-05-22 |
* | Removing useless use of metaids in tactic AST. | Pierre-Marie Pédrot | 2014-05-22 |
* | Removing decompose record / sum from the tactic AST. | Pierre-Marie Pédrot | 2014-05-21 |
* | Moving left & right tactics out of the AST. | Pierre-Marie Pédrot | 2014-05-21 |
* | Moving (e)transitivity out of the AST. | Pierre-Marie Pédrot | 2014-05-20 |
* | Tentative to add constr-using primitive tactics without grammar rules. | Pierre-Marie Pédrot | 2014-05-20 |
* | Moving argument-free tactics out of the AST into a dedicated | Pierre-Marie Pédrot | 2014-05-16 |
* | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau | 2014-05-06 |
* | Closing bug #3260 | Julien Forest | 2014-04-14 |
* | Getting rid of casted_open_constr. It was only used by the | Pierre-Marie Pédrot | 2013-11-30 |
* | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot | 2013-11-27 |
* | cList.index is now cList.index_f, same for index0 | letouzey | 2013-10-23 |
* | Revising r16550 about providing intro patterns for applying injection: | herbelin | 2013-07-09 |
* | Reorganizing intropatterns: * and ** are not naming intropatterns. | herbelin | 2013-07-09 |
* | Revert "parse "of" as KEYID "of"" | gareuselesinge | 2013-06-21 |
* | parse "of" as KEYID "of" | gareuselesinge | 2013-06-19 |
* | cbn can be called by Eval | pboutill | 2013-03-25 |
* | Restrict (try...with...) to avoid catching critical exn (part 9) | letouzey | 2013-03-13 |
* | New implementation of the conversion test, using normalization by evaluation to | mdenes | 2013-01-22 |
* | Yet a new reduction tactic in Coq : cbn | pboutill | 2012-12-21 |
* | More monomorphizations | ppedrot | 2012-11-13 |
* | remove useless hidden_flag in TacMutual(Co)Fix | letouzey | 2012-10-06 |
* | Moved Compat to parsing. This permits to break the dependency of the | ppedrot | 2012-10-04 |
* | Moving Utils.list_* to a proper CList module, which includes stdlib | ppedrot | 2012-09-14 |
* | Updating headers. | herbelin | 2012-08-08 |
* | Bigint: new functions of_int and to_int, 2nd arg of pow in int | letouzey | 2012-08-02 |
* | destruct: full compatibility with former _eqn syntax | letouzey | 2012-07-09 |
* | The tactic remember now accepts a final eqn:H option (grant wish #2489) | letouzey | 2012-07-09 |
* | induction/destruct : nicer syntax for generating equations (solves #2741) | letouzey | 2012-07-09 |
* | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot | 2012-06-22 |
* | Basic stuff about constr_expr migrated from topconstr to constrexpr_ops | letouzey | 2012-05-29 |
* | Migrate the grammar entry about "Ltac" into g_vernac.ml4. | letouzey | 2012-05-29 |
* | New files intf/constrexpr.mli and intf/notation_term.mli out of Topconstr | letouzey | 2012-05-29 |
* | Glob_term now mli-only, operations now in Glob_ops | letouzey | 2012-05-29 |
* | Tacexpr as a mli-only, the few functions there are now in Tacops | letouzey | 2012-05-29 |
* | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey | 2012-05-29 |
* | Tactic unfold always asks for comma between names. | pboutill | 2012-05-09 |
* | remove undocumented and scarcely-used tactic auto decomp | letouzey | 2012-04-23 |
* | info_trivial, info_auto, info_eauto, and debug (trivial|auto) | letouzey | 2012-03-30 |
* | Remove code of obsolete tactics : superauto, autotdb, cdhyp, dhyp, dconcl | letouzey | 2012-03-30 |
* | Noise for nothing | pboutill | 2012-03-02 |
* | Added an pattern / occurence syntax for vm_compute. | ppedrot | 2012-01-30 |
* | Applying Tom Prince's patch to support parametric "constructor n" in | herbelin | 2011-10-25 |
* | Rename rawterm.ml into glob_term.ml | glondu | 2010-12-23 |