summaryrefslogtreecommitdiff
path: root/theories/Program
diff options
context:
space:
mode:
Diffstat (limited to 'theories/Program')
-rw-r--r--theories/Program/Basics.v4
-rw-r--r--theories/Program/Combinators.v4
-rw-r--r--theories/Program/Equality.v4
-rw-r--r--theories/Program/Program.v4
-rw-r--r--theories/Program/Subset.v4
-rw-r--r--theories/Program/Syntax.v4
-rw-r--r--theories/Program/Tactics.v4
-rw-r--r--theories/Program/Utils.v8
-rw-r--r--theories/Program/Wf.v4
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. *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-06 22:48:42 +0000