From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- contrib/correctness/examples/Handbook.v | 2 +- contrib/correctness/examples/exp.v | 2 +- contrib/correctness/examples/exp_int.v | 2 +- contrib/correctness/examples/fact.v | 2 +- contrib/correctness/examples/fact_int.v | 2 +- 5 files changed, 5 insertions(+), 5 deletions(-) (limited to 'contrib/correctness/examples') diff --git a/contrib/correctness/examples/Handbook.v b/contrib/correctness/examples/Handbook.v index 8c983a72..abb1cc76 100644 --- a/contrib/correctness/examples/Handbook.v +++ b/contrib/correctness/examples/Handbook.v @@ -8,7 +8,7 @@ (* Certification of Imperative Programs / Jean-Christophe Filliātre *) -(* $Id: Handbook.v,v 1.3 2001/04/11 07:56:19 filliatr Exp $ *) +(* $Id: Handbook.v 1577 2001-04-11 07:56:19Z filliatr $ *) (* This file contains proofs of programs taken from the * "Handbook of Theoretical Computer Science", volume B, diff --git a/contrib/correctness/examples/exp.v b/contrib/correctness/examples/exp.v index dcfcec87..3142e906 100644 --- a/contrib/correctness/examples/exp.v +++ b/contrib/correctness/examples/exp.v @@ -8,7 +8,7 @@ (* Certification of Imperative Programs / Jean-Christophe Filliātre *) -(*i $Id: exp.v,v 1.3 2001/04/11 07:56:19 filliatr Exp $ i*) +(*i $Id: exp.v 1577 2001-04-11 07:56:19Z filliatr $ i*) (* Efficient computation of X^n using * diff --git a/contrib/correctness/examples/exp_int.v b/contrib/correctness/examples/exp_int.v index accd60c2..044263ca 100644 --- a/contrib/correctness/examples/exp_int.v +++ b/contrib/correctness/examples/exp_int.v @@ -8,7 +8,7 @@ (* Certification of Imperative Programs / Jean-Christophe Filliātre *) -(* $Id: exp_int.v,v 1.4 2001/04/11 07:56:19 filliatr Exp $ *) +(* $Id: exp_int.v 1577 2001-04-11 07:56:19Z filliatr $ *) (* Efficient computation of X^n using * diff --git a/contrib/correctness/examples/fact.v b/contrib/correctness/examples/fact.v index e480c806..07e77140 100644 --- a/contrib/correctness/examples/fact.v +++ b/contrib/correctness/examples/fact.v @@ -8,7 +8,7 @@ (* Certification of Imperative Programs / Jean-Christophe Filliātre *) -(* $Id: fact.v,v 1.3 2001/04/11 07:56:19 filliatr Exp $ *) +(* $Id: fact.v 1577 2001-04-11 07:56:19Z filliatr $ *) (* Proof of an imperative program computing the factorial (over type nat) *) diff --git a/contrib/correctness/examples/fact_int.v b/contrib/correctness/examples/fact_int.v index cb2b0460..f463ca80 100644 --- a/contrib/correctness/examples/fact_int.v +++ b/contrib/correctness/examples/fact_int.v @@ -8,7 +8,7 @@ (* Certification of Imperative Programs / Jean-Christophe Filliātre *) -(* $Id: fact_int.v,v 1.3 2001/04/11 07:56:19 filliatr Exp $ *) +(* $Id: fact_int.v 1577 2001-04-11 07:56:19Z filliatr $ *) (* Proof of an imperative program computing the factorial (over type Z) *) -- cgit v1.2.3