aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2013-08-09Fix batch compilation of scripts with Admitted proofs (in a section)gareuselesinge
2013-08-09fix batch compilation of scripts containing Admittedgareuselesinge
2013-08-08stm: (initial) support for -coq-slavesgareuselesinge
2013-08-08get rid of closures in global/proof stategareuselesinge
2013-08-08enhance marshallable option for freeze (minor TODO in safe_typing)gareuselesinge
2013-08-08Vernac classification streamlined (handles VERNAC EXTEND)gareuselesinge
2013-08-08Simple machinery to detect EXTEND that interpret during parsinggareuselesinge
2013-08-08Support Proof Generalgareuselesinge
2013-08-08Coqide ported to STMgareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-08-06Added more flags choice in desambiguating printer. The code isppedrot
2013-08-05Tentative fix for bug #2961. When we have to print two terms thatppedrot
2013-08-04Fixing #2846: Uncaught exception Reduction.NotArity.ppedrot
2013-08-04Removing useless casts between arrays and lists.ppedrot
2013-08-03Replacing uses of association lists by maps in notations.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-01Granting bug #3098: adding priority to Existing Instances.ppedrot
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-17Declaremods: major refactoring, stop duplicating libobjects in modulesletouzey
2013-07-17More dynamic argument scopesletouzey
2013-07-10Added a Register Inline command for the native compiler. Will be ported to th...mdenes
2013-07-02Removing the use of leveled tactics wit_tacticn. It is now handledppedrot
2013-06-24Using the whole tactic environment while Pretyping.ppedrot
2013-06-22Generalizing the use of maps instead of lists in the interpretationppedrot
2013-06-21Cutting the dependency of Genarg in constr_expr, glob_constrppedrot
2013-06-06Fixing bug #3030.ppedrot
2013-06-06More comments in Genarg.ppedrot
2013-06-06Add an option to shrink the context of program obligations to avoidmsozeau
2013-06-05Replacing lists by maps in matching interpretation.ppedrot
2013-06-02Making the behavior of "injection ... as ..." more natural:herbelin
2013-05-30Removing a useless location in ltac trace mechanism.ppedrot
2013-05-28Getting rid of LtacLocated exception transformer.ppedrot
2013-05-14Replacing Id.check with Id.is_valid, as its sole use was underppedrot
2013-05-12Use the Hook module here and there.ppedrot
2013-05-09Use definition_entry to declare local definitionsgareuselesinge
2013-05-09Getting rid of module Gmapl.ppedrot
2013-05-09A uniformization step around understand_* and interp_* functions.herbelin
2013-05-09Uniformization: isevars -> evdref/sigma/evdherbelin
2013-05-09Fixing r16487 on sharing evars between multiple parameters (missing List.rev).herbelin
2013-05-08Uniformizing the [if_warn] flag used for warning printing and putppedrot
2013-05-08Declaration of multiple hypotheses or parameters now share typingherbelin
2013-05-08Share more information between constructors and arity of an inductiveherbelin
2013-05-06New module Xml_printer (dual to Xml_parser)gareuselesinge
2013-05-06States: frozen states can hold closuresgareuselesinge
2013-05-06Close the .glob file after having saved .vogareuselesinge
2013-05-05Improvement of r16204 on reporting tactic error locations: if the mainherbelin
2013-04-29Merging Context and Sign.ppedrot
2013-04-29Splitting Term into five unrelated interfaces:ppedrot
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-25 15:35:53 +0000