aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-08-04Added test for bug #2846.ppedrot
2013-08-04Fixing #2846: Uncaught exception Reduction.NotArity.ppedrot
2013-08-04Added a test for bug #3062.ppedrot
2013-08-04Fixing #3062. Computation of the value of a fresh identifier wasppedrot
2013-08-04Removing useless casts between arrays and lists.ppedrot
2013-08-04Removing now useless merging primitives from Evd.ppedrot
2013-08-04Small cleaning of printing coercion failures in Ltac interpretation.ppedrot
2013-08-03Small fixes due to the arrival of OCaml 3.12.ppedrot
2013-08-03Replacing uses of association lists by maps in notations.ppedrot
2013-08-03Replacing an association list by a map in globalizing environment.ppedrot
2013-08-02Adding a dependent version of equal_f, thus fixing #3074.ppedrot
2013-08-02Small typo in Print Debug GCppedrot
2013-08-01Added a Print Debug GC command that displays the current state ofppedrot
2013-08-01Added a test for bug #3088.ppedrot
2013-08-01Fixing #3088. Translation from globconstrs to patterns was forgettingppedrot
2013-08-01Documenting the Remove Hints command.ppedrot
2013-08-01Added printing of instance priority to the Print Instances command.ppedrot
2013-08-01Documenting the previous commit: Existing Instance with priority.ppedrot
2013-08-01Granting bug #3098: adding priority to Existing Instances.ppedrot
2013-07-31Typo in definition clos_reflppedrot
2013-07-30Granting wish #1781:ppedrot
2013-07-29Tentative fix for #3054: we refresh universes in a term generatedppedrot
2013-07-29better error message for unexpected renaming (closes #2987)gareuselesinge
2013-07-29Revert "Only arguments declared as implicit can be renamed"gareuselesinge
2013-07-27Protecting every call to current_term in CoqIDE so that callbackppedrot
2013-07-27Added a way to change dynamically coqtop arguments in CoqIDE.ppedrot
2013-07-26Fixing #3089. This implied tweaking the definition of the lexicographicppedrot
2013-07-25Fixing bug #3093 by adding the asked test case.ppedrot
2013-07-24Added a concat function to List theory. Strangely, it was missing.ppedrot
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-17Declaremods: major refactoring, stop duplicating libobjects in modulesletouzey
2013-07-17Modops.destr_functor without useless envletouzey
2013-07-17Safe_typing: minor factorisationletouzey
2013-07-17Lib.contents () instead of Lib.contents_after Noneletouzey
2013-07-17More dynamic argument scopesletouzey
2013-07-17Extraction : message about lack of support for toplevel Includeletouzey
2013-07-17Pre-create typeclass_instances and rewrite hintdb in Autoletouzey
2013-07-10Added a Register Inline command for the native compiler. Will be ported to th...mdenes
2013-07-10Continuing r16621 on injection intro-patterns:herbelin
2013-07-09Revising r16550 about providing intro patterns for applying injection:herbelin
2013-07-09Reorganizing intropatterns: * and ** are not naming intropatterns.herbelin
2013-07-06Fixing a bug in the native compiler, introduced by r16363, leading to undefinedmdenes
2013-07-05Removing SortArgType.ppedrot
2013-07-05Expurgating the useless difference between List0 and List1 at theppedrot
2013-07-02Removing the use of leveled tactics wit_tacticn. It is now handledppedrot
2013-07-02Removed the ad-hod handling of wit_tacticn.ppedrot
2013-06-30Using functors to reduce the boilerplate used in registeringppedrot
2013-06-30Fixing Camlp4 compilation.ppedrot
2013-06-27Removed the distinction between generic Ltac vars and Let/Introppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-02-09 12:26:03 +0000