| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-07-22 | Fixed proof of irrelevance of le on nat, inspired by the | Maxime Dénès | |
| corresponding proof in ssreflect. | |||
| 2014-07-22 | Made intersection on regular trees less intensional. | Maxime Dénès | |
| 2014-07-22 | Refining match subterm and commutative cut rules. The parameters that are | Maxime Dénès | |
| instantiated in the return predicate are now taken into account. The resulting recargs tree is the intersection between the one of the branches and the appearing in the return predicate. Both the domain and co-domain are filtered. | |||
| 2014-07-22 | Tentative fix for the commutative cut subterm rule. | Maxime Dénès | |
| Some fixpoints are now rejected in the standard library, but that's probably because we compare trees for equality instead of intersecting them. | |||
| 2014-07-22 | Tentative patch for incompatibility between subterm relation and dependent | Maxime Dénès | |
| pattern matching. This patch should be improved in two ways: (1) Implement the same checks for the commutative cut subterm rule. (2) When checking safe recursive subterms for each of the branches in a match, instanciated parameters in the return predicate should be taken into account. Step (1) should be enough to restore a correct guard condition, but (2) will be required if we don't want to rule out some legitimate and practical examples. | |||
| 2014-07-22 | Ide: Drop argument added by MacOS during .app launch | Pierre Boutillier | |
| 2014-07-22 | the art of forgetting new files during rebase -i | Pierre Boutillier | |
| 2014-07-22 | A makefile rule to build bin/CoqIDE_$VERSION.app macOS bundle | Pierre Boutillier | |
| The created bundle contains only coqide and gtk (no coqtop, no stdlib) | |||
| 2014-07-22 | Coqide use '(diraname MYSELF)/coqtop' as coqtop only if this file exists | Pierre Boutillier | |
| 2014-07-22 | When I make MacOS binary, I would like to have a coqtop able to speak to ↵ | Pierre Boutillier | |
| coqide without building coqide | |||
| 2014-07-22 | Small code sharing in TacticMatching. | Pierre-Marie Pédrot | |
| 2014-07-22 | Adding a "is_val" primitive to IStream. | Pierre-Marie Pédrot | |
| 2014-07-21 | Universe level maps use HMaps. | Pierre-Marie Pédrot | |
| 2014-07-21 | Missing primitives in HMap. | Pierre-Marie Pédrot | |
| 2014-07-21 | Fixing semantics of HSet.inter and HSet.diff. | Pierre-Marie Pédrot | |
| 2014-07-21 | More straightforward definition of Universes.add_list_map. | Pierre-Marie Pédrot | |
| 2014-07-21 | Cleanup substitution inside universe instances, only done through subst_fn now, | Matthieu Sozeau | |
| and disable hashconsing of substituted instances which had a huge performance penalty in general. They are hashconsed when put in the environment only now. | |||
| 2014-07-21 | Fixing output test-suite. | Pierre-Marie Pédrot | |
| 2014-07-21 | Correct eauto which was not dealing properly with polymorphic constants. | Matthieu Sozeau | |
| 2014-07-21 | Cleanup code for constant equality in kernel conversion. | Matthieu Sozeau | |
| 2014-07-21 | Missing space in pretty-printer | Pierre-Marie Pédrot | |
| 2014-07-21 | Documenting the changes of Locate semantics. | Pierre-Marie Pédrot | |
| 2014-07-21 | Unifying locate code, also making it more powerful: it is now able to find | Pierre-Marie Pédrot | |
| any prefix of the given qualid. | |||
| 2014-07-21 | Adding a new "Locate Term" command, distinct from the raw "Locate" command. | Pierre-Marie Pédrot | |
| The new Term version has essentially the same behaviour as the old "Locate", while the new raw searches for all types of objects. Also code merging with the "Locate Ltac". Fixes bug #3380. | |||
| 2014-07-21 | More complete printing of Ltac location, akin to the term-dedicated Locate ↵ | Pierre-Marie Pédrot | |
| command. | |||
| 2014-07-21 | Documenting the need of the "DECLARE PLUGIN" statement. | Pierre-Marie Pédrot | |
| 2014-07-21 | Documenting the change of semantics of the "constructor" tactic. | Pierre-Marie Pédrot | |
| 2014-07-21 | Adding a test-suite for bug #3422. | Pierre-Marie Pédrot | |
| 2014-07-20 | Use kernel conversion on terms that contain universe variables during ↵ | Matthieu Sozeau | |
| unification, speeding it up considerably Revert backwards-incompatible commit 77df7b1283940d979d3e14893d151bc544f41410 | |||
| 2014-07-17 | Fix coercion code to disallow using cumulativity in the domain of products, ↵ | Matthieu Sozeau | |
| which results in strange changes in user provided terms. | |||
| 2014-07-17 | Completing c236b51348d2 by fixing EqdepFactsv actually committing the | Hugo Herbelin | |
| new files (WeakFan.v and WKL.v). | |||
| 2014-07-16 | Adding a test-suite for bug #3416. | Pierre-Marie Pédrot | |
| 2014-07-16 | Fixing universe substitution in mutual fixpoints. | Pierre-Marie Pédrot | |
| 2014-07-16 | STM: check-vi-task fixed | Enrico Tassi | |
| 2014-07-16 | STM: Goal printing got wrong in a merge, fixed | Enrico Tassi | |
| 2014-07-16 | - Fix bug introduced in obligations which wouldn't consider all evars that are | Matthieu Sozeau | |
| given to the obligation making function. - Fix handling of universe context when solve_by_tac is used. | |||
| 2014-07-15 | Added a (constructive) proof of Weak Konig's lemma for decidable trees. | Hugo Herbelin | |
| Renamed Fan.v into WeakFan.v since this was a proof of Weak Fan Theorem after all. | |||
| 2014-07-15 | Some basics facts about eq_dep. | Hugo Herbelin | |
| 2014-07-15 | Using the generic timeout function in the boostrapped file. | Pierre-Marie Pédrot | |
| 2014-07-14 | Don't set global variables from a hidden file. (!) | Matthieu Sozeau | |
| 2014-07-14 | Add interface function to replace new_Type () | Matthieu Sozeau | |
| 2014-07-14 | Redo PMP's patch to rewriting to make it purely functional using state passing. | Matthieu Sozeau | |
| 2014-07-14 | smartlocate: look for the head symbol for real | Enrico Tassi | |
| This bug was hacked around in ssreflect, but with the new idea that parsing and interpretation are done in distinct phases the work around could not be implemented anymore. | |||
| 2014-07-14 | Adding a delay to tclTIME. | Pierre-Marie Pédrot | |
| 2014-07-13 | Mentioning the incompatibility due to fixing bug #2996 (see #3418). | Hugo Herbelin | |
| 2014-07-13 | Adding a "time" tactical for benchmarking purposes. In case the tactic | Hugo Herbelin | |
| backtracks, print time spent in each of successive calls. | |||
| 2014-07-11 | Fix Funind test-suite file after patch by Pierre. | Matthieu Sozeau | |
| 2014-07-11 | Properly add a Set lower bound on any polymorphic inductive in Type with | Matthieu Sozeau | |
| more than one constructor. | |||
| 2014-07-11 | An outdated comment + comment layout. | Arnaud Spiwack | |
| 2014-07-11 | STM: let toploop plugins specify the flags for STM workers | Enrico Tassi | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |