| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-07-22 | Revert "Extend subterm relation to pattern matching in return predicates." | Maxime Dénès | |
| This reverts commit ec1bb8a981fef14b58ab65483244fc42b05aef13. | |||
| 2014-07-22 | Revert "Propagate size info through pattern matching in predicates, for the" | Maxime Dénès | |
| This reverts commit 6a3bcd3ae320e65347cbd6ef4bac458f073d02ea. Apply again if this kind of dependently typed programming idioms are needed. | |||
| 2014-07-22 | Propagate size info through pattern matching in predicates, for the | Maxime Dénès | |
| commutative cut rule. The error messages of the guard checker are now sometimes not informative enough. | |||
| 2014-07-22 | Extend subterm relation to pattern matching in return predicates. | Maxime Dénès | |
| A pattern matching is can now be a subterm if: - Every branch is a subterm - The return predicate is a pattern matching whose return predicate is an arity. - That pattern matching (in the return predicate) returns the same inductive family in the conclusion of each branch. The commutative cut rule hasn't been updated accordingly yet. | |||
| 2014-07-22 | Fix check_inductive_codomain. | Maxime Dénès | |
| 2014-07-22 | Refine check_is_subterm. | Maxime Dénès | |
| Following Bruno's suggestion, we check if the tree expected for the recursive argument is included in the one which is inferred. This check is probably not necessary in the current state of affairs, but might become so after further extensions of the guard condition. | |||
| 2014-07-22 | Refined guard condition of cofixpoints, to anticipate potential futur | Maxime Dénès | |
| extensions. | |||
| 2014-07-22 | First attempt at a fix for guard condition on cofixpoints. | Maxime Dénès | |
| 2014-07-22 | Add test-suite file for guard condition on cofixpoints. | Maxime Dénès | |
| 2014-07-22 | Typo in comment. | Maxime Dénès | |
| 2014-07-22 | Simplified rect2, it turns out Arthur's trick was not required. | Maxime Dénès | |
| Standard library now compiles fully. | |||
| 2014-07-22 | A version of Fin.rect2 that is compatible with the fix of the guard condition. | Maxime Dénès | |
| Thanks to Arthur Azevedo de Amorim! | |||
| 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 | |
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |