aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
* Printing any backtrace in debug mode, not only anomalies.Gravatar ppedrot2013-08-10
* Small typosGravatar ppedrot2013-08-10
* Lemmas ending with Defined cannot be delegated to slavesGravatar gareuselesinge2013-08-10
* Adding the processed tag to comments in CoqIDE.Gravatar ppedrot2013-08-09
* Fix batch compilation of scripts with Admitted proofs (in a section)Gravatar gareuselesinge2013-08-09
* checker validation fixed w.r.t. FuturesGravatar gareuselesinge2013-08-09
* checker validation made a bit more verboseGravatar gareuselesinge2013-08-09
* fix batch compilation of scripts containing AdmittedGravatar gareuselesinge2013-08-09
* state_id data typeGravatar gareuselesinge2013-08-09
* Gtk check_buttons do have a labelGravatar gareuselesinge2013-08-08
* calling interp by hand is forbiddenGravatar gareuselesinge2013-08-08
* Add a (very minimal) Proof General mode to CoqIDEGravatar gareuselesinge2013-08-08
* stm: (initial) support for -coq-slavesGravatar gareuselesinge2013-08-08
* get rid of closures in global/proof stateGravatar gareuselesinge2013-08-08
* enhance marshallable option for freeze (minor TODO in safe_typing)Gravatar gareuselesinge2013-08-08
* Test for Paral-ITPGravatar gareuselesinge2013-08-08
* Vernac classification streamlined (handles VERNAC EXTEND)Gravatar gareuselesinge2013-08-08
* Simple machinery to detect EXTEND that interpret during parsingGravatar gareuselesinge2013-08-08
* Support Proof GeneralGravatar gareuselesinge2013-08-08
* Coqide ported to STMGravatar gareuselesinge2013-08-08
* Fix testsuite so that it works with STMGravatar gareuselesinge2013-08-08
* Manual fixed w.r.t. STMGravatar gareuselesinge2013-08-08
* State Transaction MachineGravatar gareuselesinge2013-08-08
* Side effect free implementation of admit (Isabelle's oracle)Gravatar gareuselesinge2013-08-08
* Vcs data structure (Git inspired builder for Dag)Gravatar gareuselesinge2013-08-08
* Dag data structureGravatar gareuselesinge2013-08-08
* Searchable stack data structureGravatar gareuselesinge2013-08-08
* Future library to represent pure computationsGravatar gareuselesinge2013-08-08
* Fixing a warning in CoqIDE compilation.Gravatar ppedrot2013-08-08
* Small fix in IStream interface.Gravatar ppedrot2013-08-08
* Removing association lists in Constrintern.Gravatar ppedrot2013-08-07
* Added more flags choice in desambiguating printer. The code isGravatar ppedrot2013-08-06
* Tentative fix for bug #2961. When we have to print two terms thatGravatar ppedrot2013-08-05
* Added test for bug #2846.Gravatar ppedrot2013-08-04
* Fixing #2846: Uncaught exception Reduction.NotArity.Gravatar ppedrot2013-08-04
* Added a test for bug #3062.Gravatar ppedrot2013-08-04
* Fixing #3062. Computation of the value of a fresh identifier wasGravatar ppedrot2013-08-04
* Removing useless casts between arrays and lists.Gravatar ppedrot2013-08-04
* Removing now useless merging primitives from Evd.Gravatar ppedrot2013-08-04
* Small cleaning of printing coercion failures in Ltac interpretation.Gravatar ppedrot2013-08-04
* Small fixes due to the arrival of OCaml 3.12.Gravatar ppedrot2013-08-03
* Replacing uses of association lists by maps in notations.Gravatar ppedrot2013-08-03
* Replacing an association list by a map in globalizing environment.Gravatar ppedrot2013-08-03
* Adding a dependent version of equal_f, thus fixing #3074.Gravatar ppedrot2013-08-02
* Small typo in Print Debug GCGravatar ppedrot2013-08-02
* Added a Print Debug GC command that displays the current state ofGravatar ppedrot2013-08-01
* Added a test for bug #3088.Gravatar ppedrot2013-08-01
* Fixing #3088. Translation from globconstrs to patterns was forgettingGravatar ppedrot2013-08-01
* Documenting the Remove Hints command.Gravatar ppedrot2013-08-01
* Added printing of instance priority to the Print Instances command.Gravatar ppedrot2013-08-01
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-05 10:33:00 +0000