aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/formula.ml4
-rw-r--r--plugins/firstorder/formula.mli2
-rw-r--r--plugins/firstorder/instances.ml2
-rw-r--r--plugins/firstorder/rules.mli4
-rw-r--r--plugins/firstorder/sequent.ml12
-rw-r--r--plugins/firstorder/sequent.mli6
-rw-r--r--plugins/firstorder/unify.mli2
7 files changed, 12 insertions, 20 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index db1a46a03..c55040df0 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -8,7 +8,7 @@
open Hipattern
open Names
-open Term
+open Constr
open EConstr
open Vars
open Termops
@@ -39,7 +39,7 @@ exception Is_atom of constr
let meta_succ m = m+1
let rec nb_prod_after n c=
- match kind_of_term c with
+ match Constr.kind c with
| Prod (_,_,b) ->if n>0 then nb_prod_after (n-1) b else
1+(nb_prod_after 0 b)
| _ -> 0
diff --git a/plugins/firstorder/formula.mli b/plugins/firstorder/formula.mli
index 106c469c6..3b6b711c0 100644
--- a/plugins/firstorder/formula.mli
+++ b/plugins/firstorder/formula.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Term
+open Constr
open EConstr
open Globnames
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index c2606dbe8..3409471a7 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -24,7 +24,7 @@ open Misctypes
open Context.Rel.Declaration
let compare_instance inst1 inst2=
- let cmp c1 c2 = OrderedConstr.compare (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in
+ let cmp c1 c2 = Constr.compare (EConstr.Unsafe.to_constr c1) (EConstr.Unsafe.to_constr c2) in
match inst1,inst2 with
Phantom(d1),Phantom(d2)->
(cmp d1 d2)
diff --git a/plugins/firstorder/rules.mli b/plugins/firstorder/rules.mli
index d8d4c1a38..5c46f4cec 100644
--- a/plugins/firstorder/rules.mli
+++ b/plugins/firstorder/rules.mli
@@ -6,9 +6,9 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Term
-open EConstr
open Names
+open Constr
+open EConstr
open Globnames
type tactic = unit Proofview.tactic
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 05194164b..ea2d076ed 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -54,13 +54,7 @@ struct
(priority e1.pat) - (priority e2.pat)
end
-module OrderedConstr=
-struct
- type t=Term.constr
- let compare=Term.compare
-end
-
-type h_item = global_reference * (int*Term.constr) option
+type h_item = global_reference * (int*Constr.t) option
module Hitem=
struct
@@ -70,13 +64,13 @@ struct
if c = 0 then
let cmp (i1, c1) (i2, c2) =
let c = Int.compare i1 i2 in
- if c = 0 then OrderedConstr.compare c1 c2 else c
+ if c = 0 then Constr.compare c1 c2 else c
in
Option.compare cmp co1 co2
else c
end
-module CM=Map.Make(OrderedConstr)
+module CM=Map.Make(Constr)
module History=Set.Make(Hitem)
diff --git a/plugins/firstorder/sequent.mli b/plugins/firstorder/sequent.mli
index ca6079c8b..7f4a6dd86 100644
--- a/plugins/firstorder/sequent.mli
+++ b/plugins/firstorder/sequent.mli
@@ -10,11 +10,9 @@ open EConstr
open Formula
open Globnames
-module OrderedConstr: Set.OrderedType with type t=Term.constr
+module CM: CSig.MapS with type key=Constr.t
-module CM: CSig.MapS with type key=Term.constr
-
-type h_item = global_reference * (int*Term.constr) option
+type h_item = global_reference * (int*Constr.t) option
module History: Set.S with type elt = h_item
diff --git a/plugins/firstorder/unify.mli b/plugins/firstorder/unify.mli
index d3e8aeee8..390aa8c85 100644
--- a/plugins/firstorder/unify.mli
+++ b/plugins/firstorder/unify.mli
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-open Term
+open Constr
open EConstr
exception UFAIL of constr*constr