aboutsummaryrefslogtreecommitdiff
path: root/toplevel
AgeCommit message (Expand)Author
2013-09-06Moving Searchstack to CStack, and normalizing names a bit.ppedrot
2013-09-03Partly replacing list-based access functions in Evd. This is stillppedrot
2013-08-30summary for ML modules made correctgareuselesinge
2013-08-30Make the jopin-document button wait for slaves to terminategareuselesinge
2013-08-30When PG is used as interface behave as before STMgareuselesinge
2013-08-30ind_tables: properly handling side effectsgareuselesinge
2013-08-30Stm: if slave process dies badly go back to local lazy evaluationgareuselesinge
2013-08-30-coq-slaves: close_on_exec + correct argument passinggareuselesinge
2013-08-28Fixing bug #3083.ppedrot
2013-08-25Added a more efficient way to recover the domain of a map.ppedrot
2013-08-22Misc changes around coqtop.ml :letouzey
2013-08-22Less "Coq" strings everywhereletouzey
2013-08-20Fix STM: Module Import may change the parsergareuselesinge
2013-08-20Universe counters on slaves are in sync with mastergareuselesinge
2013-08-20Declarations.mli: reorganization of modular structuresletouzey
2013-08-20Himsg : strict 80-column indentationletouzey
2013-08-20Safe_typing code refactoringletouzey
2013-08-19Modulification and removing of structural equality in Stateid.ppedrot
2013-08-19Modulification and removing of structural equality in VCS.ppedrot
2013-08-12Fixing potentially misused Errors.push.ppedrot
2013-08-11Mutual proofs cannot be delegatedgareuselesinge
2013-08-10Small typosppedrot
2013-08-10Lemmas ending with Defined cannot be delegated to slavesgareuselesinge
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-26 02:05:07 +0000