diff options
author | Stephane Glondu <steph@glondu.net> | 2011-12-25 13:19:42 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2011-12-25 13:19:42 +0100 |
commit | 300293c119981054c95182a90c829058530a6b6f (patch) | |
tree | d7303613741c5796b58ced7db24ec7203327dbb2 /theories/Program | |
parent | 9d27ae09786866b6e3d7b79d1fa7667e5e2aa309 (diff) |
Imported Upstream version 8.3.pl3upstream/8.3.pl3
Diffstat (limited to 'theories/Program')
-rw-r--r-- | theories/Program/Basics.v | 4 | ||||
-rw-r--r-- | theories/Program/Combinators.v | 4 | ||||
-rw-r--r-- | theories/Program/Equality.v | 4 | ||||
-rw-r--r-- | theories/Program/Program.v | 4 | ||||
-rw-r--r-- | theories/Program/Subset.v | 4 | ||||
-rw-r--r-- | theories/Program/Syntax.v | 4 | ||||
-rw-r--r-- | theories/Program/Tactics.v | 4 | ||||
-rw-r--r-- | theories/Program/Utils.v | 8 | ||||
-rw-r--r-- | theories/Program/Wf.v | 4 |
9 files changed, 20 insertions, 20 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index a298032f..37c4d94d 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -1,12 +1,12 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Basics.v 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: Basics.v 14641 2011-11-06 11:59:10Z herbelin $ *) (** Standard functions and combinators. diff --git a/theories/Program/Combinators.v b/theories/Program/Combinators.v index e61c7027..f446b455 100644 --- a/theories/Program/Combinators.v +++ b/theories/Program/Combinators.v @@ -1,12 +1,12 @@ (* -*- coding: utf-8 -*- *) (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Combinators.v 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: Combinators.v 14641 2011-11-06 11:59:10Z herbelin $ *) (** * Proofs about standard combinators, exports functional extensionality. diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index b9eb8f80..f63aad43 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Equality.v 13730 2010-12-19 13:32:01Z msozeau $ i*) +(*i $Id: Equality.v 14641 2011-11-06 11:59:10Z herbelin $ i*) (** Tactics related to (dependent) equality and proof irrelevance. *) diff --git a/theories/Program/Program.v b/theories/Program/Program.v index 929fc47c..2b6dd864 100644 --- a/theories/Program/Program.v +++ b/theories/Program/Program.v @@ -1,11 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Program.v 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: Program.v 14641 2011-11-06 11:59:10Z herbelin $ *) Require Export Coq.Program.Utils. Require Export Coq.Program.Wf. diff --git a/theories/Program/Subset.v b/theories/Program/Subset.v index 9d82fde8..d0a76d3f 100644 --- a/theories/Program/Subset.v +++ b/theories/Program/Subset.v @@ -1,11 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Subset.v 13323 2010-07-24 15:57:30Z herbelin $ *) +(* $Id: Subset.v 14641 2011-11-06 11:59:10Z herbelin $ *) (** Tactics related to subsets and proof irrelevance. *) diff --git a/theories/Program/Syntax.v b/theories/Program/Syntax.v index 2f89ff53..582bc461 100644 --- a/theories/Program/Syntax.v +++ b/theories/Program/Syntax.v @@ -1,11 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Syntax.v 13492 2010-10-04 21:20:01Z herbelin $ *) +(* $Id: Syntax.v 14641 2011-11-06 11:59:10Z herbelin $ *) (** Custom notations and implicits for Coq prelude definitions. diff --git a/theories/Program/Tactics.v b/theories/Program/Tactics.v index 4a41d9c9..f62ff703 100644 --- a/theories/Program/Tactics.v +++ b/theories/Program/Tactics.v @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Tactics.v 13693 2010-12-08 15:32:25Z msozeau $ i*) +(*i $Id: Tactics.v 14641 2011-11-06 11:59:10Z herbelin $ i*) (** This module implements various tactics used to simplify the goals produced by Program, which are also generally useful. *) diff --git a/theories/Program/Utils.v b/theories/Program/Utils.v index b2b5d4be..1e57a74b 100644 --- a/theories/Program/Utils.v +++ b/theories/Program/Utils.v @@ -1,12 +1,12 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Utils.v 13323 2010-07-24 15:57:30Z herbelin $ i*) +(*i $Id: Utils.v 14641 2011-11-06 11:59:10Z herbelin $ i*) (** Various syntaxic shortands that are useful with [Program]. *) @@ -28,7 +28,7 @@ Delimit Scope program_scope with prg. (** Abbreviation for first projection and hiding of proofs of subset objects. *) -Notation " ` t " := (proj1_sig t) (at level 10, t at next level) : program_scope. +Notation " ` t " := (proj1_sig t) (at level 10, t at next level) : program_scope. (** Coerces objects to their support before comparing them. *) @@ -55,4 +55,4 @@ Extract Inductive bool => "bool" [ "true" "false" ]. Extract Inductive sumbool => "bool" [ "true" "false" ]. (* Extract Inductive prod "'a" "'b" => " 'a * 'b " [ "(,)" ]. *) (* Extract Inductive sigT => "prod" [ "" ]. *) -*)
\ No newline at end of file +*) diff --git a/theories/Program/Wf.v b/theories/Program/Wf.v index 4ca49c41..3afaf5e8 100644 --- a/theories/Program/Wf.v +++ b/theories/Program/Wf.v @@ -1,11 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: Wf.v 13492 2010-10-04 21:20:01Z herbelin $ *) +(* $Id: Wf.v 14641 2011-11-06 11:59:10Z herbelin $ *) (** Reformulation of the Wf module using subsets where possible, providing the support for [Program]'s treatment of well-founded definitions. *) |