diff options
Diffstat (limited to 'theories/Program')
| -rw-r--r-- | theories/Program/Basics.v | 2 | ||||
| -rw-r--r-- | theories/Program/Equality.v | 2 | ||||
| -rw-r--r-- | theories/Program/FunctionalExtensionality.v | 2 |
3 files changed, 3 insertions, 3 deletions
diff --git a/theories/Program/Basics.v b/theories/Program/Basics.v index 1129c5b65e..8f1f26dbcd 100644 --- a/theories/Program/Basics.v +++ b/theories/Program/Basics.v @@ -13,7 +13,7 @@ * Institution: LRI, CNRS UMR 8623 - UniversitĂcopyright Paris Sud * 91405 Orsay, France *) -(* $Id: FSetAVL_prog.v 616 2007-08-08 12:28:10Z msozeau $ *) +(* $Id$ *) (** The polymorphic identity function. *) diff --git a/theories/Program/Equality.v b/theories/Program/Equality.v index 46a1b5cf25..0f88fbdd93 100644 --- a/theories/Program/Equality.v +++ b/theories/Program/Equality.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Permut.v 9245 2006-10-17 12:53:34Z notin $ i*) +(*i $Id$ i*) (** Tactics related to (dependent) equality and proof irrelevance. *) diff --git a/theories/Program/FunctionalExtensionality.v b/theories/Program/FunctionalExtensionality.v index c2a6f3df6c..440217bfec 100644 --- a/theories/Program/FunctionalExtensionality.v +++ b/theories/Program/FunctionalExtensionality.v @@ -7,7 +7,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: Tactics.v 10410 2007-12-31 13:11:55Z msozeau $ i*) +(*i $Id$ i*) (** This module states the axiom of (dependent) functional extensionality and (dependent) eta-expansion. It introduces a tactic [extensionality] to apply the axiom of extensionality to an equality goal. |