| Age | Commit message (Expand) | Author |
|---|
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-06-04 | Replacing some str with strbrk | ppedrot |
| 2012-06-01 | Cleaning Pp.ppnl use | ppedrot |
| 2012-06-01 | Getting rid of Pp.msgnl and Pp.message. | ppedrot |
| 2012-05-30 | More uniformisation in Pp.warn functions. | ppedrot |
| 2012-05-29 | global_reference migrated from Libnames to new Globnames, less deps in gramma... | letouzey |
| 2012-05-29 | Basic stuff about constr_expr migrated from topconstr to constrexpr_ops | letouzey |
| 2012-05-29 | slim down a bit genarg.ml (pr_intro_pattern forgotten there) | letouzey |
| 2012-05-29 | Pattern as a mli-only file, operations in Patternops | 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-04-23 | remove undocumented and scarcely-used tactic auto decomp | letouzey |
| 2012-04-18 | Corrects a (very) longstanding bug of tactics. As is were, tactic expecting | aspiwack |
| 2012-04-18 | Adds the openconstr entry for tactic notations. | aspiwack |
| 2012-04-18 | Better error message in tactic notations. | aspiwack |
| 2012-03-30 | 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-20 | Continuing r15045-15046 and r15055 (fixing bug #2732 about atomic | herbelin |
| 2012-03-14 | Revise API of understand_ltac to be parameterized by a flag for resolution of... | msozeau |
| 2012-03-14 | Second step of integration of Program: | msozeau |
| 2012-03-02 | Noise for nothing | pboutill |
| 2012-01-30 | Added an pattern / occurence syntax for vm_compute. | ppedrot |
| 2012-01-20 | Breakpoints in Ltac debugger: new command "r foo" to jump to the next | herbelin |
| 2011-12-17 | Improving pretty-printing of Ltac functions. | herbelin |
| 2011-11-17 | Fixing bug #2640 and variants of it (inconsistency between when and | herbelin |
| 2011-11-02 | Add type annotations around all calls to Libobject.declare_object | letouzey |
| 2011-10-28 | Remove dynamic stuff from constr_expr and glob_constr | glondu |
| 2011-10-25 | Applying Tom Prince's patch to support parametric "constructor n" in | herbelin |
| 2011-09-26 | Added support for referring to subterms of the goal by pattern. | herbelin |
| 2011-09-26 | Moving implicit tactic support from Tacinterp to Pfedit and final evar | herbelin |
| 2011-07-29 | generic = on named_context replaced by named_context_equal | puech |
| 2011-05-17 | More work on error handling | letouzey |
| 2011-04-28 | Revert r14078 "Partial backtrack on the support for open terms in destruct/in... | gmelquio |
| 2011-04-28 | Partial backtrack on the support for open terms in destruct/induction: | gmelquio |
| 2011-04-14 | More informative anomaly. | herbelin |
| 2011-04-13 | Revert "Add [Polymorphic] flag for defs" | msozeau |
| 2011-04-13 | - Remove create_evar_defs | msozeau |
| 2011-04-13 | Add [Polymorphic] flag for defs | msozeau |
| 2011-03-18 | A tatical "timeout <n> <tac>" that fails if <tac> hasn't finished in <n> seconds | letouzey |
| 2011-02-10 | Rename subst_raw_with_bindings to subst_glob_with_bindings and export | msozeau |
| 2010-12-23 | Rename rawterm.ml into glob_term.ml | glondu |
| 2010-12-23 | Change of nomenclature: rawconstr -> glob_constr | glondu |
| 2010-10-31 | An experimental support for open constrs in hints and in "using" | herbelin |
| 2010-09-24 | Some dead code removal, thanks to Oug analyzer | letouzey |
| 2010-09-11 | Improving a few error messages in Ltac interpretation | herbelin |
| 2010-07-30 | Capitulation wrt "change pat with term": instead of solving the | herbelin |
| 2010-07-28 | oops. commited files I shouldn't have. reverting on r13341 | barras |
| 2010-07-28 | ported r13340 to trunk | barras |
