| Commit message (Expand) | Author | Age |
|---|
| * | admit: replaced by give_up + Admitted (no proof_admitted : False, close #4032) |  Enrico Tassi | 2015-03-11 |
| * | More expressive API for tclWITHHOLES. |  Pierre-Marie Pédrot | 2015-02-10 |
| * | Revert "Removing spurious tclWITHHOLES." | Pierre-Marie Pédrot | 2015-02-10 |
| * | Update headers. |  Maxime Dénès | 2015-01-12 |
| * | Getting rid of Exninfo hacks. | Pierre-Marie Pédrot | 2014-12-16 |
| * | Moving change_in_concl, change_in_hyp, change_concl to Proofview.tactic. |  Hugo Herbelin | 2014-12-07 |
| * | Used an evar name based on the local def name in "evar" tactic. | Hugo Herbelin | 2014-11-25 |
| * | new: Optimize Proof, Optimize Heap | Enrico Tassi | 2014-11-09 |
| * | Removing the legacy intro tactic code. | Pierre-Marie Pédrot | 2014-11-07 |
| * | Change reduction_of_red_expr to return an e_reduction_function returning |  Matthieu Sozeau | 2014-10-24 |
| * | Proofview: split [V82] module into [Unsafe] and [V82]. |  Arnaud Spiwack | 2014-10-22 |
| * | Remove the deprecated open-constr based refine. | Arnaud Spiwack | 2014-10-22 |
| * | Proofview.Refine: remove the handle type, and simplify the API. | Arnaud Spiwack | 2014-10-16 |
| * | Splitting out of auto.ml a file hints.ml dedicated to hints so as to | Hugo Herbelin | 2014-10-07 |
| * | Add syntax for naming new goals in refine: writing ?[id] instead of _ | Hugo Herbelin | 2014-09-30 |
| * | Merging some functions from evarutil.ml/evd.ml. | Hugo Herbelin | 2014-09-29 |
| * | Keyed unification option, compiling the whole standard library | Matthieu Sozeau | 2014-09-27 |
| * | Rename eq_constr functions in Evd to not break backward compatibility | Matthieu Sozeau | 2014-09-24 |
| * | 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-17 |
| * | 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-12 |
| * | Add a tactic [revgoals] to reverse the list of focused goals. | Arnaud Spiwack | 2014-09-08 |
| * | Renaming goal-entering functions. | Pierre-Marie Pédrot | 2014-09-06 |
| * | 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-05 |
| * | Moving the decompose tactic out of the AST. | Pierre-Marie Pédrot | 2014-09-01 |
| * | Removing spurious tclWITHHOLES. | Pierre-Marie Pédrot | 2014-08-27 |
| * | Add an is_cofix tactic |  Jason Gross | 2014-08-25 |
| * | Removing a use of Goal.refine. | Pierre-Marie Pédrot | 2014-08-19 |
| * | Slight simplification of naming of tactics in equality.ml (hopefully). | Hugo Herbelin | 2014-08-18 |
| * | Reorganization of tactics: | Hugo Herbelin | 2014-08-18 |
| * | Better structure for Ltac pretyping environments. | Pierre-Marie Pédrot | 2014-08-07 |
| * | [uconstr]: use a closure instead of eager substitution. | Arnaud Spiwack | 2014-08-06 |
| * | 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-05 |
| * | Add [guard] tactic. | Arnaud Spiwack | 2014-08-01 |
| * | 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-07-25 |
| * | Moved code for finding subterms (pattern, induction, set, generalize, ...) | Hugo Herbelin | 2014-06-28 |
| * | Oops, I fixed the .ml's |  Matthieu Sozeau | 2014-06-23 |
| * | Proofs now take and return an evar_universe_context, simplifying interfaces | Matthieu Sozeau | 2014-06-18 |
| * | Removing decompose record / sum from the tactic AST. | Pierre-Marie Pédrot | 2014-05-21 |
| * | Now parsing rules of ML-declared tactics are only made available after the | Pierre-Marie Pédrot | 2014-05-12 |
| * | - 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-05-06 |
| * | Removing the compatibility layer from Leminv. Also removed an undocumented | Pierre-Marie Pédrot | 2014-04-22 |
| * | Closing bug #3260 |  Julien Forest | 2014-04-14 |
Enrico Tassi
Pierre-Marie Pédrot
Maxime Dénès
Hugo Herbelin
Matthieu Sozeau
Arnaud Spiwack
Jason Gross
Matthieu Sozeau
Julien Forest