diff options
Diffstat (limited to 'contrib/correctness/pcic.mli')
| -rw-r--r-- | contrib/correctness/pcic.mli | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/contrib/correctness/pcic.mli b/contrib/correctness/pcic.mli index 21c3839d9..f0b629071 100644 --- a/contrib/correctness/pcic.mli +++ b/contrib/correctness/pcic.mli @@ -8,13 +8,13 @@ (* Certification of Imperative Programs / Jean-Christophe Filliātre *) -(* $Id$ *) +(*i $Id$ i*) open Past -open Term +open Rawterm -(* transforms intermediate functional programs into CIC terms *) +(* transforms intermediate functional programs into (raw) CIC terms *) -val constr_of_prog : cc_term -> constr +val rawconstr_of_prog : cc_term -> rawconstr |