diff options
Diffstat (limited to 'src/trace/smtForm.ml')
-rw-r--r-- | src/trace/smtForm.ml | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/src/trace/smtForm.ml b/src/trace/smtForm.ml index 12aef5a..044ff4c 100644 --- a/src/trace/smtForm.ml +++ b/src/trace/smtForm.ml @@ -80,11 +80,11 @@ module type FORM = val clear : reify -> unit val get : ?declare:bool -> reify -> pform -> t - (** Give a coq term, build the corresponding formula *) + (** Given a coq term, build the corresponding formula *) val of_coq : (Structures.constr -> hatom) -> reify -> Structures.constr -> t val hash_hform : (hatom -> hatom) -> reify -> t -> t - (** Flattening of [Fand] and [For], removing of [Fnot2] *) + (* Flattening of [Fand] and [For], removing of [Fnot2] *) val flatten : reify -> t -> t (** Turn n-ary [Fand] and [For] into their right-associative @@ -100,10 +100,10 @@ module type FORM = val to_array : reify -> 'a -> (pform -> 'a) -> int * 'a array val interp_tbl : reify -> Structures.constr * Structures.constr val nvars : reify -> int - (** Producing a Coq term corresponding to the interpretation - of a formula *) - (** [interp_atom] map [hatom] to coq term, it is better if it produce - shared terms. *) + (* Producing a Coq term corresponding to the interpretation + of a formula *) + (* [interp_atom] map [hatom] to coq term, it is better if it produce + shared terms. *) val interp_to_coq : (hatom -> Structures.constr) -> (int, Structures.constr) Hashtbl.t -> t -> Structures.constr @@ -589,9 +589,9 @@ module Make (Atom:ATOM) = (mkInt i, Structures.mkArray (Lazy.force cform, t)) let nvars reify = reify.count - (** Producing a Coq term corresponding to the interpretation of a formula *) - (** [interp_atom] map [Atom.t] to coq term, it is better if it produce - shared terms. *) + (* Producing a Coq term corresponding to the interpretation of a formula *) + (* [interp_atom] map [Atom.t] to coq term, it is better if it produce + shared terms. *) let interp_to_coq interp_atom form_tbl f = let rec interp_form f = let l = to_lit f in |