| Age | Commit message (Expand) | Author |
|---|
| 2013-11-30 | Fixing ltac constr variable handling in refine. | Pierre-Marie Pédrot |
| 2013-11-30 | Getting rid of casted_open_constr. It was only used by the | Pierre-Marie Pédrot |
| 2013-11-27 | Adding generic solvers to term holes. For now, no resolution mechanism nor | Pierre-Marie Pédrot |
| 2013-11-25 | Remove the Hiddentac module. | Arnaud Spiwack |
| 2013-11-02 | Doc: solve the bad interaction between Declare Implicit Tactic and refine. | aspiwack |
| 2013-11-02 | Refine: Tactics.New.refine does beta-reduction. | aspiwack |
| 2013-11-02 | Adds a tactic give_up. | aspiwack |
| 2013-11-02 | A tactic shelve_unifiable. | aspiwack |
| 2013-11-02 | Adds a shelve tactic. | aspiwack |
| 2013-11-02 | Refine does beta-reductions. | aspiwack |
| 2013-11-02 | Less use of the list-based interface for goal-bound tactics. | aspiwack |
| 2013-11-02 | Tachmach.New is now in Proofview.Goal.enter style. | aspiwack |
| 2013-11-02 | More Proofview.Goal.enter. | aspiwack |
| 2013-11-02 | Clean up a warning. | aspiwack |
| 2013-11-02 | The tactic [admit] exits with the "unsafe" status. | aspiwack |
| 2013-11-02 | A whole new implemenation of the refine tactic. | aspiwack |
| 2013-11-02 | Clean-up: removed redundant notations (>>-) and (>>--) from Proofview.Notations. | aspiwack |
| 2013-11-02 | Getting rid of Goal.here, and all the related exceptions and combinators. | aspiwack |
| 2013-11-02 | Makes the new Proofview.tactic the basic type of Ltac. | aspiwack |
| 2013-10-05 | Moving side effects into evar_map. There was no reason to keep another | ppedrot |
| 2013-08-08 | Vernac classification streamlined (handles VERNAC EXTEND) | gareuselesinge |
| 2013-08-08 | State Transaction Machine | gareuselesinge |
| 2013-06-04 | Start documenting new [rewrite_strat] tactic that applies rewriting | msozeau |
| 2013-06-02 | Making the behavior of "injection ... as ..." more natural: | herbelin |
| 2013-05-12 | Granting wish #3014: | ppedrot |
| 2013-04-29 | Splitting Term into five unrelated interfaces: | ppedrot |
| 2013-04-22 | code simplifications concerning Summary | letouzey |
| 2013-03-13 | Restrict (try...with...) to avoid catching critical exn (part 13) | letouzey |
| 2013-02-18 | Removing Exc_located and using the new exception enrichement | ppedrot |
| 2013-01-28 | Uniformization of the "anomaly" command. | ppedrot |
| 2012-12-14 | Modulification of identifier | ppedrot |
| 2012-12-08 | Finish patch for Hint Resolve, stopping to generate new constant names for | msozeau |
| 2012-11-25 | Monomorphization (tactics) | ppedrot |
| 2012-10-26 | Change Hint Resolve, Immediate to take a global reference as argument | msozeau |
| 2012-10-15 | Continue killing hidden tactics : no more generated h_xxx | letouzey |
| 2012-10-02 | Remove some more "open" and dead code thanks to OCaml4 warnings | letouzey |
| 2012-09-14 | As r15801: putting everything from Util.array_* to CArray.*. | ppedrot |
| 2012-08-08 | Updating headers. | herbelin |
| 2012-06-22 | Added an indirection with respect to Loc in Compat. As many [open Compat] | ppedrot |
| 2012-06-01 | Getting rid of Pp.msgnl and Pp.message. | ppedrot |
| 2012-05-31 | tactic is_fix, akin to is_evar, is_hyp, is_ ... family | pboutill |
| 2012-05-30 | Getting rid of Pp.msg | ppedrot |
| 2012-05-29 | place all files specific to camlp4 syntax extensions in grammar/ | letouzey |
| 2012-05-29 | Basic stuff about constr_expr migrated from topconstr to constrexpr_ops | letouzey |
| 2012-05-29 | Glob_term now mli-only, operations now in Glob_ops | letouzey |
| 2012-05-29 | locus.mli for occurrences+clauses, misctypes.mli for various little things | letouzey |
| 2012-05-29 | Evar_kinds.mli containing former Evd.hole_kind, avoid deps on Evd | letouzey |
| 2012-04-17 | Remove the Dp plugin. | gmelquio |
| 2012-03-14 | Second step of integration of Program: | msozeau |
| 2012-03-02 | Noise for nothing | pboutill |
