Skip to content


Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
Commits on Jul 22, 2014
  1. Minor cleaning.

  2. Revert "Propagate size info through pattern matching in predicates, f…

    …or the"
    This reverts commit 6a3bcd3.
    Apply again if this kind of dependently typed programming idioms are needed.
  3. Propagate size info through pattern matching in predicates, for the

    commutative cut rule.
    The error messages of the guard checker are now sometimes not
    informative enough.
  4. Extend subterm relation to pattern matching in return predicates.

    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.
  5. Refine check_is_subterm.

    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.
  6. Typo in comment.

  7. Simplified rect2, it turns out Arthur's trick was not required.

    Standard library now compiles fully.
  8. A version of Fin.rect2 that is compatible with the fix of the guard c…

    Thanks to Arthur Azevedo de Amorim!
  9. Fixed proof of irrelevance of le on nat, inspired by the

    corresponding proof in ssreflect.
  10. Refining match subterm and commutative cut rules. The parameters that…

    … are
    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.
  11. Tentative fix for the commutative cut subterm rule.

    Some fixpoints are now rejected in the standard library, but that's probably
    because we compare trees for equality instead of intersecting them.
  12. Tentative patch for incompatibility between subterm relation and depe…

    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.
  13. @pirbo
  14. @pirbo
  15. @pirbo

    A makefile rule to build bin/CoqIDE_$ macOS bundle

    pirbo authored
    The created bundle contains only coqide and gtk (no coqtop, no stdlib)
  16. @pirbo
  17. @pirbo

    When I make MacOS binary, I would like to have a coqtop able to speak…

    pirbo authored
    … to coqide without building coqide
  18. @ppedrot
  19. @ppedrot
Commits on Jul 21, 2014
  1. @ppedrot

    Universe level maps use HMaps.

    ppedrot authored
  2. @ppedrot

    Missing primitives in HMap.

    ppedrot authored
  3. @ppedrot
  4. @ppedrot
  5. @mattam82

    Cleanup substitution inside universe instances, only done through sub…

    mattam82 authored
    …st_fn now,
    and disable hashconsing of substituted instances which had a huge performance
    penalty in general. They are hashconsed when put in the environment only now.
  6. @ppedrot

    Fixing output test-suite.

    ppedrot authored
  7. @mattam82
  8. @mattam82
  9. @ppedrot
Something went wrong with that request. Please try again.