diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-01 14:45:20 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2008-04-01 14:45:20 +0000 |
| commit | 124016815a5a38dfebee75451721ae13bca81959 (patch) | |
| tree | b3adc59b7ecc5fb6093e21a741bf764fa206864f /theories/Program | |
| parent | 97fb9f22eadab06fe320ccedf6abfb6be89702f4 (diff) | |
Ajout des propriétés $Id:$ là où elles n'existaient pas ou n'étaient
pas correctes
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10739 85f007b7-540e-0410-9357-904b9bb8a0f7
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 1129c5b65..8f1f26dbc 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 46a1b5cf2..0f88fbdd9 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 c2a6f3df6..440217bfe 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. |