| Age | Commit message (Expand) | Author |
|---|
| 2013-07-19 | - Fix uncaught exception NotASort from reductionops, moving decomp_sort to re... | msozeau |
| 2013-07-17 | "Boolean Equality" and "Case Analysis" are already off by default... | letouzey |
| 2013-07-17 | Declaremods: major refactoring, stop duplicating libobjects in modules | letouzey |
| 2013-07-17 | Modops.destr_functor without useless env | letouzey |
| 2013-07-17 | Safe_typing: minor factorisation | letouzey |
| 2013-07-17 | Lib.contents () instead of Lib.contents_after None | letouzey |
| 2013-07-17 | More dynamic argument scopes | letouzey |
| 2013-07-17 | Extraction : message about lack of support for toplevel Include | letouzey |
| 2013-07-17 | Pre-create typeclass_instances and rewrite hintdb in Auto | letouzey |
| 2013-07-10 | Added a Register Inline command for the native compiler. Will be ported to th... | mdenes |
| 2013-07-10 | Continuing r16621 on injection intro-patterns: | herbelin |
| 2013-07-09 | Revising r16550 about providing intro patterns for applying injection: | herbelin |
| 2013-07-09 | Reorganizing intropatterns: * and ** are not naming intropatterns. | herbelin |
| 2013-07-06 | Fixing a bug in the native compiler, introduced by r16363, leading to undefined | mdenes |
| 2013-07-05 | Removing SortArgType. | ppedrot |
| 2013-07-05 | Expurgating the useless difference between List0 and List1 at the | ppedrot |
| 2013-07-02 | Removing the use of leveled tactics wit_tacticn. It is now handled | ppedrot |
| 2013-07-02 | Removed the ad-hod handling of wit_tacticn. | ppedrot |
| 2013-06-30 | Using functors to reduce the boilerplate used in registering | ppedrot |
| 2013-06-30 | Fixing Camlp4 compilation. | ppedrot |
| 2013-06-27 | Removed the distinction between generic Ltac vars and Let/Intro | ppedrot |
| 2013-06-27 | Added a generic handler of Ltac quotations, based on the existing | ppedrot |
| 2013-06-27 | Getting rid of IntroPatternArgType. | ppedrot |
| 2013-06-27 | Removing useless tactic arguments, and using generic arguments | ppedrot |
| 2013-06-27 | Bugfix: Fixing #3050 | ppedrot |
| 2013-06-25 | Useless use of maps in constr internalizing. | ppedrot |
| 2013-06-24 | Cleaning up the type of Tacinterp.extract_ltac_constr_values. | ppedrot |
| 2013-06-24 | Using the whole tactic environment while Pretyping. | ppedrot |
| 2013-06-22 | Now, idtac closures use maps instead of association list. | ppedrot |
| 2013-06-22 | Fixing the semantics of the previous patch. | ppedrot |
| 2013-06-22 | Generalizing the use of maps instead of lists in the interpretation | ppedrot |
| 2013-06-21 | Splitted up Genarg in four different levels: | ppedrot |
| 2013-06-21 | Cutting the dependency of Genarg in constr_expr, glob_constr | ppedrot |
| 2013-06-21 | Revert "KEYID token makes parsing more robust in face of notations" | gareuselesinge |
| 2013-06-21 | Revert "parse "of" as KEYID "of"" | gareuselesinge |
| 2013-06-19 | Moving wit_unit to Stdarg. | ppedrot |
| 2013-06-19 | Adding genarg printer to debugger. | ppedrot |
| 2013-06-19 | Fixing argument extension. Instead of qualified names, string | ppedrot |
| 2013-06-19 | - Keep the refinement of existing evars comming from unification with a rewri... | msozeau |
| 2013-06-19 | parse "of" as KEYID "of" | gareuselesinge |
| 2013-06-19 | KEYID token makes parsing more robust in face of notations | gareuselesinge |
| 2013-06-18 | Proof-of-concept: moved four easy-to-handle generic arguments to | ppedrot |
| 2013-06-18 | Removing the various glob/subst/interp registering functions for | ppedrot |
| 2013-06-18 | Implementing a new interface for Genarg, with centralized data | ppedrot |
| 2013-06-18 | Now glob_sign and interp_sign only depend on structures defined | ppedrot |
| 2013-06-17 | Documenting a potential source of incompleteness in the ring tactic, | amahboub |
| 2013-06-14 | Exporting field f_debug (needed for Ssreflect). | ppedrot |
| 2013-06-14 | Using an "extra" Store.t field in interp_sign instead of dedicated | ppedrot |
| 2013-06-14 | When doing setoid_rewrite through rewrite, do resolution of classes | msozeau |
| 2013-06-13 | Normalizing exception raised by tactic coercions. | ppedrot |
