diff options
| author | filliatr | 1999-08-30 07:27:52 +0000 |
|---|---|---|
| committer | filliatr | 1999-08-30 07:27:52 +0000 |
| commit | 19d21ec59b69a7bd5a8e4e77794e85fed6b48d39 (patch) | |
| tree | 4d6a784866d8b8da5a8c4378b3ce3fdf9d159186 /lib/hashcons.mli | |
| parent | 72681a66688b1b81309582cfaf979a7096a118c2 (diff) | |
un petit effort de presentation dans les interfaces
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@31 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'lib/hashcons.mli')
| -rw-r--r-- | lib/hashcons.mli | 27 |
1 files changed, 7 insertions, 20 deletions
diff --git a/lib/hashcons.mli b/lib/hashcons.mli index 76a8fba4e8..917c063e1f 100644 --- a/lib/hashcons.mli +++ b/lib/hashcons.mli @@ -1,19 +1,9 @@ -(****************************************************************************) -(* The Calculus of Inductive Constructions *) -(* *) -(* Projet Coq *) -(* *) -(* INRIA LRI-CNRS ENS-CNRS *) -(* Rocquencourt Orsay Lyon *) -(* *) -(* Coq V6.3 *) -(* July 1st 1999 *) -(* *) -(****************************************************************************) -(* hashcons.mli *) -(****************************************************************************) -val stat: unit->unit +(* $Id$ *) + +(* Generic hash-consing. *) + +val stat : unit->unit module type Comp = sig @@ -31,7 +21,7 @@ module type S = val f : unit -> (u -> t -> t) end -module Make(X:Comp): (S with type t = X.t and type u = X.u) +module Make(X:Comp) : (S with type t = X.t and type u = X.u) val simple_hcons : (unit -> 'u -> 't -> 't) -> ('u -> 't -> 't) val recursive_hcons : (unit -> ('t -> 't) * 'u -> 't -> 't) -> ('u -> 't -> 't) @@ -42,12 +32,11 @@ val recursive2_hcons : (unit -> ('t1 -> 't1) * ('t2 -> 't2) * 'u2 -> 't2 -> 't2) -> 'u1 -> 'u2 -> ('t1 -> 't1) * ('t2 -> 't2) - (* Declaring and reinitializing global hash-consing functions *) + val init : unit -> unit val register_hcons : ('u -> 't -> 't) -> ('u -> 't -> 't) - module Hstring : (S with type t = string and type u = unit) module Hobj : (S with type t = Obj.t and type u = (Obj.t -> Obj.t) * unit) @@ -56,5 +45,3 @@ val obj : Obj.t -> Obj.t val magic_hash : 'a -> 'a -(* $Id$ *) - |