diff options
| author | Matej Košík | 2017-05-29 11:02:06 +0200 |
|---|---|---|
| committer | Matej Košík | 2017-06-10 10:33:53 +0200 |
| commit | b6feaafc7602917a8ef86fb8adc9651ff765e710 (patch) | |
| tree | 5a033488c31040009adb725f20e8bd0a5dd31bc5 /plugins/firstorder/sequent.ml | |
| parent | 102d7418e399de646b069924277e4baea1badaca (diff) | |
Remove (useless) aliases from the API.
Diffstat (limited to 'plugins/firstorder/sequent.ml')
| -rw-r--r-- | plugins/firstorder/sequent.ml | 7 |
1 files changed, 3 insertions, 4 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 4a93e01dca..435ca1986e 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -7,7 +7,6 @@ (************************************************************************) open API -open Term open EConstr open CErrors open Util @@ -58,11 +57,11 @@ end module OrderedConstr= struct - type t=Constr.t - let compare=constr_ord + type t=Term.constr + let compare=Term.compare end -type h_item = global_reference * (int*Constr.t) option +type h_item = global_reference * (int*Term.constr) option module Hitem= struct |