| Commit message (Expand) | Author | Age |
... | |
* | Documenting the previous commit: Existing Instance with priority. | ppedrot | 2013-08-01 |
* | Granting bug #3098: adding priority to Existing Instances. | ppedrot | 2013-08-01 |
* | Typo in definition clos_refl | ppedrot | 2013-07-31 |
* | Granting wish #1781: | ppedrot | 2013-07-30 |
* | Tentative fix for #3054: we refresh universes in a term generated | ppedrot | 2013-07-29 |
* | better error message for unexpected renaming (closes #2987) | gareuselesinge | 2013-07-29 |
* | Revert "Only arguments declared as implicit can be renamed" | gareuselesinge | 2013-07-29 |
* | Protecting every call to current_term in CoqIDE so that callback | ppedrot | 2013-07-27 |
* | Added a way to change dynamically coqtop arguments in CoqIDE. | ppedrot | 2013-07-27 |
* | Fixing #3089. This implied tweaking the definition of the lexicographic | ppedrot | 2013-07-26 |
* | Fixing bug #3093 by adding the asked test case. | ppedrot | 2013-07-25 |
* | Added a concat function to List theory. Strangely, it was missing. | ppedrot | 2013-07-24 |
* | - Fix uncaught exception NotASort from reductionops, moving decomp_sort to re... | msozeau | 2013-07-19 |
* | "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-17 |
* | 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-10 |
* | Revising r16550 about providing intro patterns for applying injection: | herbelin | 2013-07-09 |
* | Reorganizing intropatterns: * and ** are not naming intropatterns. | herbelin | 2013-07-09 |
* | Fixing a bug in the native compiler, introduced by r16363, leading to undefined | mdenes | 2013-07-06 |
* | Removing SortArgType. | ppedrot | 2013-07-05 |
* | Expurgating the useless difference between List0 and List1 at the | ppedrot | 2013-07-05 |
* | 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-07-02 |
* | Using functors to reduce the boilerplate used in registering | ppedrot | 2013-06-30 |
* | Fixing Camlp4 compilation. | ppedrot | 2013-06-30 |
* | 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-27 |
* | Useless use of maps in constr internalizing. | ppedrot | 2013-06-25 |
* | Cleaning up the type of Tacinterp.extract_ltac_constr_values. | ppedrot | 2013-06-24 |
* | Using the whole tactic environment while Pretyping. | ppedrot | 2013-06-24 |
* | 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-22 |
* | 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-21 |
* | 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 |