aboutsummaryrefslogtreecommitdiff
AgeCommit message (Expand)Author
2014-07-22Made intersection on regular trees less intensional.Maxime Dénès
2014-07-22Refining match subterm and commutative cut rules. The parameters that areMaxime Dénès
2014-07-22Tentative fix for the commutative cut subterm rule.Maxime Dénès
2014-07-22Tentative patch for incompatibility between subterm relation and dependentMaxime Dénès
2014-07-22Ide: Drop argument added by MacOS during .app launchPierre Boutillier
2014-07-22the art of forgetting new files during rebase -iPierre Boutillier
2014-07-22A makefile rule to build bin/CoqIDE_$VERSION.app macOS bundlePierre Boutillier
2014-07-22Coqide use '(diraname MYSELF)/coqtop' as coqtop only if this file existsPierre Boutillier
2014-07-22When I make MacOS binary, I would like to have a coqtop able to speak to coqi...Pierre Boutillier
2014-07-22Small code sharing in TacticMatching.Pierre-Marie Pédrot
2014-07-22Adding a "is_val" primitive to IStream.Pierre-Marie Pédrot
2014-07-21Universe level maps use HMaps.Pierre-Marie Pédrot
2014-07-21Missing primitives in HMap.Pierre-Marie Pédrot
2014-07-21Fixing semantics of HSet.inter and HSet.diff.Pierre-Marie Pédrot
2014-07-21More straightforward definition of Universes.add_list_map.Pierre-Marie Pédrot
2014-07-21Cleanup substitution inside universe instances, only done through subst_fn now,Matthieu Sozeau
2014-07-21Fixing output test-suite.Pierre-Marie Pédrot
2014-07-21Correct eauto which was not dealing properly with polymorphic constants.Matthieu Sozeau
2014-07-21Cleanup code for constant equality in kernel conversion.Matthieu Sozeau
2014-07-21Missing space in pretty-printerPierre-Marie Pédrot
2014-07-21Documenting the changes of Locate semantics.Pierre-Marie Pédrot
2014-07-21Unifying locate code, also making it more powerful: it is now able to findPierre-Marie Pédrot
2014-07-21Adding a new "Locate Term" command, distinct from the raw "Locate" command.Pierre-Marie Pédrot
2014-07-21More complete printing of Ltac location, akin to the term-dedicated Locate co...Pierre-Marie Pédrot
2014-07-21Documenting the need of the "DECLARE PLUGIN" statement.Pierre-Marie Pédrot
2014-07-21Documenting the change of semantics of the "constructor" tactic.Pierre-Marie Pédrot
2014-07-21Adding a test-suite for bug #3422.Pierre-Marie Pédrot
2014-07-20Use kernel conversion on terms that contain universe variables during unifica...Matthieu Sozeau
2014-07-17Fix coercion code to disallow using cumulativity in the domain of products, w...Matthieu Sozeau
2014-07-17Completing c236b51348d2 by fixing EqdepFactsv actually committing theHugo Herbelin
2014-07-16Adding a test-suite for bug #3416.Pierre-Marie Pédrot
2014-07-16Fixing universe substitution in mutual fixpoints.Pierre-Marie Pédrot
2014-07-16STM: check-vi-task fixedEnrico Tassi
2014-07-16STM: Goal printing got wrong in a merge, fixedEnrico Tassi
2014-07-16- Fix bug introduced in obligations which wouldn't consider all evars that areMatthieu Sozeau
2014-07-15Added a (constructive) proof of Weak Konig's lemma for decidable trees.Hugo Herbelin
2014-07-15Some basics facts about eq_dep.Hugo Herbelin
2014-07-15Using the generic timeout function in the boostrapped file.Pierre-Marie Pédrot
2014-07-14Don't set global variables from a hidden file. (!)Matthieu Sozeau
2014-07-14Add interface function to replace new_Type ()Matthieu Sozeau
2014-07-14Redo PMP's patch to rewriting to make it purely functional using state passing.Matthieu Sozeau
2014-07-14smartlocate: look for the head symbol for realEnrico Tassi
2014-07-14Adding a delay to tclTIME.Pierre-Marie Pédrot
2014-07-13Mentioning the incompatibility due to fixing bug #2996 (see #3418).Hugo Herbelin
2014-07-13Adding a "time" tactical for benchmarking purposes. In case the tacticHugo Herbelin
2014-07-11Fix Funind test-suite file after patch by Pierre.Matthieu Sozeau
2014-07-11Properly add a Set lower bound on any polymorphic inductive in Type withMatthieu Sozeau
2014-07-11An outdated comment + comment layout.Arnaud Spiwack
2014-07-11STM: let toploop plugins specify the flags for STM workersEnrico Tassi
2014-07-11STM: flag to turn off branch reopeningEnrico Tassi
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-20 18:48:02 +0000