aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2013-08-09Adding the processed tag to comments in CoqIDE.ppedrot
2013-08-09Fix batch compilation of scripts with Admitted proofs (in a section)gareuselesinge
2013-08-09checker validation fixed w.r.t. Futuresgareuselesinge
2013-08-09checker validation made a bit more verbosegareuselesinge
2013-08-09fix batch compilation of scripts containing Admittedgareuselesinge
2013-08-09state_id data typegareuselesinge
2013-08-08Gtk check_buttons do have a labelgareuselesinge
2013-08-08calling interp by hand is forbiddengareuselesinge
2013-08-08Add a (very minimal) Proof General mode to CoqIDEgareuselesinge
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
generated by cgit v1.2.3 (git 2.25.1) at 2026-03-26 06:01:38 +0000