aboutsummaryrefslogtreecommitdiffhomepage
Commit message (Expand)AuthorAge
...
* First attempt at a fix for guard condition on cofixpoints.Gravatar Maxime Dénès2014-07-22
* Add test-suite file for guard condition on cofixpoints.Gravatar Maxime Dénès2014-07-22
* Typo in comment.Gravatar Maxime Dénès2014-07-22
* Simplified rect2, it turns out Arthur's trick was not required.Gravatar Maxime Dénès2014-07-22
* A version of Fin.rect2 that is compatible with the fix of the guard condition.Gravatar Maxime Dénès2014-07-22
* Fixed proof of irrelevance of le on nat, inspired by theGravatar Maxime Dénès2014-07-22
* Made intersection on regular trees less intensional.Gravatar Maxime Dénès2014-07-22
* Refining match subterm and commutative cut rules. The parameters that areGravatar Maxime Dénès2014-07-22
* Tentative fix for the commutative cut subterm rule.Gravatar Maxime Dénès2014-07-22
* Tentative patch for incompatibility between subterm relation and dependentGravatar Maxime Dénès2014-07-22
* Ide: Drop argument added by MacOS during .app launchGravatar Pierre Boutillier2014-07-22
* the art of forgetting new files during rebase -iGravatar Pierre Boutillier2014-07-22
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-09 23:38:02 +0000