aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
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-08Test for Paral-ITPgareuselesinge
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-08Fix testsuite so that it works with STMgareuselesinge
2013-08-08Manual fixed w.r.t. STMgareuselesinge
2013-08-08State Transaction Machinegareuselesinge
2013-08-08Side effect free implementation of admit (Isabelle's oracle)gareuselesinge
2013-08-08Vcs data structure (Git inspired builder for Dag)gareuselesinge
2013-08-08Dag data structuregareuselesinge
2013-08-08Searchable stack data structuregareuselesinge
2013-08-08Future library to represent pure computationsgareuselesinge
2013-08-08Fixing a warning in CoqIDE compilation.ppedrot
2013-08-08Small fix in IStream interface.ppedrot
2013-08-07Removing association lists in Constrintern.ppedrot
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-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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-02 08:52:20 +0000