| Age | Commit message (Expand) | Author |
|---|
| 2015-12-09 | Fixing parsing of the unshelve tactical. | Pierre-Marie Pédrot |
| 2015-12-09 | Adding an unshelve tactical. | Pierre-Marie Pédrot |
| 2015-11-27 | Fix [Polymorphic Hint Rewrite]. | Matthieu Sozeau |
| 2015-10-02 | Univs: refined handling of assumptions | Matthieu Sozeau |
| 2015-10-02 | Univs: fix evar_map handling in Hint processing. | Matthieu Sozeau |
| 2015-10-02 | Univs: fix many evar_map initializations and leaks. | Matthieu Sozeau |
| 2015-09-23 | Hopefully better names to constructors of internal_flag, as discussed | Hugo Herbelin |
| 2015-05-27 | Fix bug #4159 | Matthieu Sozeau |
| 2015-05-13 | Safer typing primitives. | Pierre-Marie Pédrot |
| 2015-04-23 | Using tclZEROMSG instead of tclZERO in several places. | Pierre-Marie Pédrot |
| 2015-04-22 | Tactical `progress` compares term up to potentially equalisable universes. | Arnaud Spiwack |
| 2015-03-11 | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) | Enrico Tassi |
| 2015-02-10 | More expressive API for tclWITHHOLES. | Pierre-Marie Pédrot |
| 2015-02-10 | Revert "Removing spurious tclWITHHOLES." | Pierre-Marie Pédrot |
| 2015-01-12 | Update headers. | Maxime Dénès |
| 2014-12-16 | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot |
| 2014-12-07 | Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic. | Hugo Herbelin |
| 2014-11-25 | Used an evar name based on the local def name in "evar" tactic. | Hugo Herbelin |
| 2014-11-09 | new: Optimize Proof, Optimize Heap | Enrico Tassi |
| 2014-11-07 | Removing the legacy intro tactic code. | Pierre-Marie Pédrot |
| 2014-10-24 | Change reduction_of_red_expr to return an e_reduction_function returning | Matthieu Sozeau |
| 2014-10-22 | Proofview: split [V82] module into [Unsafe] and [V82]. | Arnaud Spiwack |
| 2014-10-22 | Remove the deprecated open-constr based refine. | Arnaud Spiwack |
| 2014-10-16 | Proofview.Refine: remove the handle type, and simplify the API. | Arnaud Spiwack |
| 2014-10-07 | Splitting out of auto.ml a file hints.ml dedicated to hints so as to | Hugo Herbelin |
| 2014-09-30 | Add syntax for naming new goals in refine: writing ?[id] instead of _ | Hugo Herbelin |
| 2014-09-29 | Merging some functions from evarutil.ml/evd.ml. | Hugo Herbelin |
| 2014-09-27 | Keyed unification option, compiling the whole standard library | Matthieu Sozeau |
| 2014-09-24 | Rename eq_constr functions in Evd to not break backward compatibility | Matthieu Sozeau |
| 2014-09-17 | Be more conservative and keep the use of eq_constr in pretyping/ functions. | Matthieu Sozeau |
| 2014-09-17 | Fix bug #3593, making constr_eq and progress work up to | Matthieu Sozeau |
| 2014-09-17 | Revert specific syntax for primitive projections, avoiding ugly | Matthieu Sozeau |
| 2014-09-12 | Uniformisation of the order of arguments env and sigma. | Hugo Herbelin |
| 2014-09-12 | Referring to evars by names. Added a parser for evars (but parsing of | Hugo Herbelin |
| 2014-09-08 | Add a tactic [revgoals] to reverse the list of focused goals. | Arnaud Spiwack |
| 2014-09-06 | Renaming goal-entering functions. | Pierre-Marie Pédrot |
| 2014-09-05 | Remove a redundant typing phase in the [refine] tactic. | Arnaud Spiwack |
| 2014-09-05 | Ltac's [uconstr] values now use the identifier context to give names to binders. | Arnaud Spiwack |
| 2014-09-01 | Moving the decompose tactic out of the AST. | Pierre-Marie Pédrot |
| 2014-08-27 | Removing spurious tclWITHHOLES. | Pierre-Marie Pédrot |
| 2014-08-25 | Add an is_cofix tactic | Jason Gross |
| 2014-08-19 | Removing a use of Goal.refine. | Pierre-Marie Pédrot |
| 2014-08-18 | Slight simplification of naming of tactics in equality.ml (hopefully). | Hugo Herbelin |
| 2014-08-18 | Reorganization of tactics: | Hugo Herbelin |
| 2014-08-07 | Better structure for Ltac pretyping environments. | Pierre-Marie Pédrot |
| 2014-08-06 | [uconstr]: use a closure instead of eager substitution. | Arnaud Spiwack |
| 2014-08-05 | Experimentally adding an option for automatically erasing an | Hugo Herbelin |
| 2014-08-05 | STM: new "par:" goal selector, like "all:" but in parallel | Enrico Tassi |
| 2014-08-05 | The [refine] tactic now accepts [uconstr]. | Arnaud Spiwack |
| 2014-08-01 | Add [guard] tactic. | Arnaud Spiwack |
