Skip to content
Commits on Jun 8, 2016
  1. @spitters

    Merge pull request #29 from coq-contribs/v8.5

    adding "Make" and "Makefile"
    spitters committed Jun 8, 2016
  2. @spitters

    Revert "adding makefile for the benefit of contribs"

    This reverts commit d6f88cc.
    spitters committed Jun 8, 2016
Commits on Jun 7, 2016
  1. @spitters
Commits on Jun 6, 2016
  1. @matej-kosik
Commits on May 31, 2016
  1. @spitters

    Update README.md

    spitters committed May 31, 2016
Commits on May 20, 2016
  1. @spitters

    Merge pull request #26 from matej-kosik/master

    Fixing compilaton wrt. Coq 8.5 (d2f9a45)
    spitters committed May 20, 2016
Commits on May 19, 2016
  1. @matej-kosik
  2. @matej-kosik
Commits on Apr 20, 2016
  1. @aa755

    ARtrans.vo compiling

    in Coq 8.5, proofs containing admit need to end with Admitted (and not Qed or Defined)
    aa755 committed Apr 19, 2016
  2. @aa755 @aa755

    crtrans.vo is compiling via scons.

    MathClasses was copied to /usr/local/.../coq/lib/user_contribs/
    aa755 committed with aa755 Mar 22, 2016
  3. @aa755

    fully quanified imports to MathClasses.

    These references were added in the trunk branch, and therefore did not get fixed by Jason's fix to the master branch.
    aa755 committed Apr 19, 2016
Commits on Apr 19, 2016
  1. @aa755
Commits on Mar 3, 2016
  1. @robbertkrebbers

    Merge pull request #24 from bmsherman/imports

    Make import statements absolute and other small changes
    robbertkrebbers committed Mar 3, 2016
Commits on Mar 1, 2016
  1. @bmsherman
  2. @bmsherman
  3. @bmsherman

    Absolutize all [Import]s

    Use Jason Gross's `absolutize-imports.py` script to make all
    [Import] statements use absolute paths rather than just relative paths,
    which fixes errors for case-insensitive filesystems.
    See:
    https://gist.github.com/JasonGross/14decf638535a2447286
    https://github.com/JasonGross/coq-tools
    bmsherman committed Mar 1, 2016
Commits on Dec 5, 2015
  1. @spitters

    Merge pull request #22 from clarus/master

    README in MarkDown with OPAM instructions
    spitters committed Dec 5, 2015
Commits on Nov 26, 2015
  1. @clarus
Commits on Jun 8, 2015
  1. @sumahadevan

    minimal patch to compile CoRN on Mac following recent patch to MathCl…

    …asses for case-sensitive file systems (math-classes/math-classes@9330ab1); minimal patch also applies to Windows; a more comprehensive fix with complete require paths like MathClasses may be preferable
    sumahadevan committed Jun 8, 2015
Commits on May 29, 2015
  1. @spitters

    Merge pull request #20 from spitters/master

    Updating README, resolving #19
    spitters committed May 29, 2015
  2. @spitters

    Updating README, resolving #19

    spitters committed May 29, 2015
Commits on Mar 14, 2015
  1. @spitters

    Merge pull request #14 from aa755/PullReq

    3 lemmas. 1) intervals are convex 2) Min is contained in any interval containing the 2 args 3) same for max
    spitters committed Mar 14, 2015
Commits on Feb 25, 2015
  1. @spitters

    Merge pull request #5 from clarus/master

    Preparation for Opam
    spitters committed Feb 25, 2015
Commits on Jan 9, 2015
  1. added 2 lemmas. Min and Max are contained in any interval containing …

    …the 2 arguments.
    Abhishek Anand committed Jan 9, 2015
  2. added a simple lemma stating convexity of [interval]s

    Abhishek Anand committed Jan 9, 2015
Commits on Dec 30, 2014
  1. @robbertkrebbers

    Merge pull request #13 from aa755/PullReq

    added the Weak_IVTQ lemma which is a stronger variant of Weak_IVT
    robbertkrebbers committed Dec 30, 2014
  2. removed some unnecessary hints and lemmas

    Abhishek Anand committed Dec 29, 2014
  3. added the Weak_IVTQ lemma which is a stronger variant of CoRN.ftc.Str…

    …ongIVT.Weak_IVT
    Abhishek Anand committed Dec 29, 2014
Commits on Sep 25, 2014
  1. @clarus
  2. @clarus

    Required old file added back

    clarus committed Sep 25, 2014
  3. @clarus

    SConstruct is back

    clarus committed Sep 25, 2014
  4. @clarus

    rational.ml not used anymore

    clarus committed Sep 25, 2014
  5. @spitters

    Remoing obsolete tactic

    spitters committed Sep 25, 2014
  6. @spitters
  7. @spitters

    Removing unused tactics

    spitters committed Sep 25, 2014
Something went wrong with that request. Please try again.