| Age | Commit message (Expand) | Author |
|---|
| 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 |
| 2014-07-25 | Add a tactic [swap i j] to swap the position of goals [i] and [j]. | Arnaud Spiwack |
| 2014-07-25 | Adds a cycle tactic to reorder goals in a loop. | Arnaud Spiwack |
| 2014-06-28 | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin |
| 2014-06-23 | Oops, I fixed the .ml's | Matthieu Sozeau |
| 2014-06-18 | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau |
| 2014-05-21 | Removing decompose record / sum from the tactic AST. | Pierre-Marie Pédrot |
| 2014-05-12 | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot |
| 2014-05-06 | - Fix bug preventing apply from unfolding Fixpoints. | Matthieu Sozeau |
| 2014-05-06 | This commit adds full universe polymorphism and fast projections to Coq. | Matthieu Sozeau |
| 2014-04-22 | Removing the compatibility layer from Leminv. Also removed an undocumented | Pierre-Marie Pédrot |
| 2014-04-14 | Closing bug #3260 | Julien Forest |
| 2014-03-31 | Removing the Change_evar refiner rule. | Pierre-Marie Pédrot |
| 2014-03-26 | Moving some tactic code to the new engine. | Pierre-Marie Pédrot |
| 2014-02-27 | Proofview.Notations: Now that (>>=) is free, use it for tclBIND. | Arnaud Spiwack |
| 2014-02-27 | Get rid of the enterl/glist API for Proofview.Goal. | Arnaud Spiwack |
| 2014-01-10 | Exporting the full pretyper options in Goal.constr_of_raw. | Pierre-Marie Pédrot |
| 2013-12-01 | Ensuring the right parsing of glob arguments, used by refine | Pierre-Marie Pédrot |
| 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 |
