| Age | Commit message (Collapse) | Author | |
|---|---|---|---|
| 2014-07-24 | Revert "Adding a "is_val" primitive to IStream." | Pierre-Marie Pédrot | |
| This reverts commit 062d07eb5446c1032fda232b9a09e20e5410dd92. | |||
| 2014-07-24 | fixup fakeide test-suite | Pierre Boutillier | |
| 2014-07-24 | Make MacStore like coqide more | Pierre Boutillier | |
| including bigger icons | |||
| 2014-07-23 | Derive plugin: document new syntax. | Arnaud Spiwack | |
| 2014-07-23 | Derive plugin: add some comments. | Arnaud Spiwack | |
| 2014-07-23 | Derive plugin: code reorganisation for clarity. | Arnaud Spiwack | |
| 2014-07-23 | Derive plugin: small refactoring. | Arnaud Spiwack | |
| 2014-07-23 | Derive plugin: a more general interface. | Arnaud Spiwack | |
| Instead of forcing the specifying property to be of the form (r spec def), allow any lemma depending on def. | |||
| 2014-07-23 | When closing a proof, make sure that the types have their evar substituted. | Arnaud Spiwack | |
| When starting proofs with [start_dependent_proof], we may have initial goals with existential variables in their conclusion. They will be solved by the proof, but this information was not propagated in close proof, and the kernel failed on uninstanciated evars. | |||
| 2014-07-23 | Proof_global: an unused variable replaced by a wildcard. | Arnaud Spiwack | |
| 2014-07-23 | Proof_global.start_dependent_proof: properly threads the sigma through the ↵ | Arnaud Spiwack | |
| telescope. Allows for a more refined notion of dependently generated initial goals. | |||
| 2014-07-23 | Change the interface of proof_global to take an evar_map instead of a ↵ | Arnaud Spiwack | |
| universe context to start proofs. It was kind of awkward to work with for non-traditionnal kinds of proofs: if you have an evar_universe_context, you got it from a sigma anyway. | |||
| 2014-07-22 | Porting guard fix to checker. | Maxime Dénès | |
| 2014-07-22 | Minor cleaning. | Maxime Dénès | |
| 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. | |||
 |
index : coq | |
| The formal proof system |
| aboutsummaryrefslogtreecommitdiff |