diff options
Diffstat (limited to 'contrib/correctness/examples')
| -rw-r--r-- | contrib/correctness/examples/Handbook.v | 2 | ||||
| -rw-r--r-- | contrib/correctness/examples/exp.v | 2 | ||||
| -rw-r--r-- | contrib/correctness/examples/exp_int.v | 2 | ||||
| -rw-r--r-- | contrib/correctness/examples/fact.v | 2 | ||||
| -rw-r--r-- | contrib/correctness/examples/fact_int.v | 2 |
5 files changed, 5 insertions, 5 deletions
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) *) |