aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* A makefile rule to build bin/CoqIDE_$VERSION.app macOS bundleGravatar Pierre Boutillier2014-07-22
* Coqide use '(diraname MYSELF)/coqtop' as coqtop only if this file existsGravatar Pierre Boutillier2014-07-22
* When I make MacOS binary, I would like to have a coqtop able to speak to coqi...Gravatar Pierre Boutillier2014-07-22
* Small code sharing in TacticMatching.Gravatar Pierre-Marie Pédrot2014-07-22
* Adding a "is_val" primitive to IStream.Gravatar Pierre-Marie Pédrot2014-07-22
* Universe level maps use HMaps.Gravatar Pierre-Marie Pédrot2014-07-21
* Missing primitives in HMap.Gravatar Pierre-Marie Pédrot2014-07-21
* Fixing semantics of HSet.inter and HSet.diff.Gravatar Pierre-Marie Pédrot2014-07-21
* More straightforward definition of Universes.add_list_map.Gravatar Pierre-Marie Pédrot2014-07-21
* Cleanup substitution inside universe instances, only done through subst_fn now,Gravatar Matthieu Sozeau2014-07-21
* Fixing output test-suite.Gravatar Pierre-Marie Pédrot2014-07-21
* Correct eauto which was not dealing properly with polymorphic constants.Gravatar Matthieu Sozeau2014-07-21
* Cleanup code for constant equality in kernel conversion.Gravatar Matthieu Sozeau2014-07-21
* Missing space in pretty-printerGravatar Pierre-Marie Pédrot2014-07-21
* Documenting the changes of Locate semantics.Gravatar Pierre-Marie Pédrot2014-07-21
* Unifying locate code, also making it more powerful: it is now able to findGravatar Pierre-Marie Pédrot2014-07-21
* Adding a new "Locate Term" command, distinct from the raw "Locate" command.Gravatar Pierre-Marie Pédrot2014-07-21
* More complete printing of Ltac location, akin to the term-dedicated Locate co...Gravatar Pierre-Marie Pédrot2014-07-21
* Documenting the need of the "DECLARE PLUGIN" statement.Gravatar Pierre-Marie Pédrot2014-07-21
* Documenting the change of semantics of the "constructor" tactic.Gravatar Pierre-Marie Pédrot2014-07-21
* Adding a test-suite for bug #3422.Gravatar Pierre-Marie Pédrot2014-07-21
* Use kernel conversion on terms that contain universe variables during unifica...Gravatar Matthieu Sozeau2014-07-20
* Fix coercion code to disallow using cumulativity in the domain of products, w...Gravatar Matthieu Sozeau2014-07-17
* Completing c236b51348d2 by fixing EqdepFactsv actually committing theGravatar Hugo Herbelin2014-07-17
* Adding a test-suite for bug #3416.Gravatar Pierre-Marie Pédrot2014-07-16
* Fixing universe substitution in mutual fixpoints.Gravatar Pierre-Marie Pédrot2014-07-16
* STM: check-vi-task fixedGravatar Enrico Tassi2014-07-16
* STM: Goal printing got wrong in a merge, fixedGravatar Enrico Tassi2014-07-16
* - Fix bug introduced in obligations which wouldn't consider all evars that areGravatar Matthieu Sozeau2014-07-16
* Added a (constructive) proof of Weak Konig's lemma for decidable trees.Gravatar Hugo Herbelin2014-07-15
* Some basics facts about eq_dep.Gravatar Hugo Herbelin2014-07-15
* Using the generic timeout function in the boostrapped file.Gravatar Pierre-Marie Pédrot2014-07-15
* Don't set global variables from a hidden file. (!)Gravatar Matthieu Sozeau2014-07-14
* Add interface function to replace new_Type ()Gravatar Matthieu Sozeau2014-07-14
* Redo PMP's patch to rewriting to make it purely functional using state passing.Gravatar Matthieu Sozeau2014-07-14
* smartlocate: look for the head symbol for realGravatar Enrico Tassi2014-07-14
* Adding a delay to tclTIME.Gravatar Pierre-Marie Pédrot2014-07-14
* Mentioning the incompatibility due to fixing bug #2996 (see #3418).Gravatar Hugo Herbelin2014-07-13
* Adding a "time" tactical for benchmarking purposes. In case the tacticGravatar Hugo Herbelin2014-07-13
* Fix Funind test-suite file after patch by Pierre.Gravatar Matthieu Sozeau2014-07-11
* Properly add a Set lower bound on any polymorphic inductive in Type withGravatar Matthieu Sozeau2014-07-11
* An outdated comment + comment layout.Gravatar Arnaud Spiwack2014-07-11
* STM: let toploop plugins specify the flags for STM workersGravatar Enrico Tassi2014-07-11
* STM: flag to turn off branch reopeningGravatar Enrico Tassi2014-07-11
* STM: add optionally takes the id of the new tipGravatar Enrico Tassi2014-07-11
* STM: export the observe function (useful for pide)Gravatar Enrico Tassi2014-07-11
* Feedback: LoadedFile + GoalsGravatar Enrico Tassi2014-07-11
* Export type_of_global_ref (useful for external users of glob files)Gravatar Enrico Tassi2014-07-11
* make the standard logging facility stm awareGravatar Enrico Tassi2014-07-11
* MSetRBT: unfortunate typo in compare_height (fix #3413)Gravatar Pierre Letouzey2014-07-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-15 05:37:51 +0000