diff options
Diffstat (limited to 'src/trace/smtForm.mli')
| -rw-r--r-- | src/trace/smtForm.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/trace/smtForm.mli b/src/trace/smtForm.mli index 2a00228..c372bf5 100644 --- a/src/trace/smtForm.mli +++ b/src/trace/smtForm.mli @@ -37,7 +37,6 @@ type fop = | Fiff | Fite | Fnot2 of int - type ('a,'f) gen_pform = | Fatom of 'a @@ -73,7 +72,7 @@ module type FORM = (** Given a coq term, build the corresponding formula *) val of_coq : (Term.constr -> hatom) -> reify -> Term.constr -> t - + (** Flattening of [Fand] and [For], removing of [Fnot2] *) val flatten : reify -> t -> t |