Commits

Breadcrumbs

History for

on49d8c0f

User selector

All users

Datepicker

All time

Commit History

Commits on Aug 21, 2012

• Now compiles with Coq 8.4

  EvgenyMakarov

  committed
  4358e01

  Copy full SHA for 4358e01

Commits on Oct 14, 2011

• Pfew, resolved all names, s/Zero/[0]/ and s/One/[1]/

  wires

  committed
  5314875

  Copy full SHA for 5314875

Commits on Feb 14, 2011

• CoRN no longer depends on Ssreflect.

  Show description for 779b5b9
  robbertkrebbers

  committed
  779b5b9

  Copy full SHA for 779b5b9

Commits on Feb 11, 2011

• More occurrences of the old fact replaced

  robbertkrebbers

  committed
  9574d8a

  Copy full SHA for 9574d8a

Commits on Oct 17, 2009

• Make almost everything compile with Matthieu's Coq-dev branch and François' "completely unofficial pre-alpha version of ssreflect1.2 working with coq trunk".

  Show description for c61d667
  Eelis

  committed
  c61d667

  Copy full SHA for c61d667

Commits on Sep 24, 2009

• Make all proof scripts ssreflect-compatible, and require&export ssreflect in algebra/Basics.

  Eelis

  committed
  4860de7

  Copy full SHA for 4860de7

Commits on Sep 23, 2009

• Use consistent layout (in particular indentation) in all proof scripts.

  Eelis

  committed
  0c00fde

  Copy full SHA for 0c00fde

Commits on Sep 15, 2009

• Now compiles with ssreflect.

  Show description for 9473954
  

  Bas Spitters

  committed
  9473954

  Copy full SHA for 9473954

Commits on Oct 31, 2008

• Fixing up coercions.

  

  Russell O'Connor

  committed
  5fd1c77

  Copy full SHA for 5fd1c77

Commits on Aug 30, 2008

• Putting RSetoid at the bottom of all hierarchies.

  

  Russell O'Connor

  committed
  8b37745

  Copy full SHA for 8b37745

Commits on Aug 27, 2008

• Adding tactic for solve Coq real number inequalites

  Show description for 6be72a6
  

  Russell O'Connor

  committed
  6be72a6

  Copy full SHA for 6be72a6

Commits on Jul 9, 2008

• One more lemma from Cezary.

  Show description for 801558b
  

  Russell O'Connor

  committed
  801558b

  Copy full SHA for 801558b

Commits on Jul 3, 2008

• More coq_real lemmas

  Show description for 4ed9c7a
  

  Russell O'Connor

  committed
  4ed9c7a

  Copy full SHA for 4ed9c7a

Commits on Apr 30, 2008

• Updated to work on latest Coq trunk

  Show description for aa0e701
  

  Russell O'Connor

  committed
  aa0e701

  Copy full SHA for aa0e701

Commits on Mar 18, 2008

• Removed some documenation headers from coq_reals.

  Show description for b383b82
  

  Russell O'Connor

  committed
  b383b82

  Copy full SHA for b383b82

Commits on Mar 12, 2008

• Adding documenation for coq_reals

  Show description for ff5e740
  

  Russell O'Connor

  committed
  ff5e740

  Copy full SHA for ff5e740

Commits on Jan 30, 2008

• Fix RReals_iso

  Show description for 8d8f51d
  

  Cezary Kaliszyk

  committed
  8d8f51d

  Copy full SHA for 8d8f51d

• RReals Isomorphism

  Show description for 5bcca05
  

  Cezary Kaliszyk

  committed
  5bcca05

  Copy full SHA for 5bcca05

• RReals

  Show description for 8a79241
  

  Cezary Kaliszyk

  committed
  8a79241

  Copy full SHA for 8a79241

Loading