diff options
Diffstat (limited to 'plugins/firstorder/sequent.ml')
| -rw-r--r-- | plugins/firstorder/sequent.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml index 2d18b66054..435ca1986e 100644 --- a/plugins/firstorder/sequent.ml +++ b/plugins/firstorder/sequent.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open API open EConstr open CErrors open Util @@ -57,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 @@ -227,7 +227,7 @@ let extend_with_auto_hints env sigma l seq = try searchtable_map dbname with Not_found-> - error ("Firstorder: "^dbname^" : No such Hint database") in + user_err Pp.(str ("Firstorder: "^dbname^" : No such Hint database")) in Hint_db.iter g hdb in List.iter h l; !seqref, sigma (*FIXME: forgetting about universes*) |