aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder/formula.ml
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder/formula.ml')
-rw-r--r--plugins/firstorder/formula.ml9
1 files changed, 5 insertions, 4 deletions
diff --git a/plugins/firstorder/formula.ml b/plugins/firstorder/formula.ml
index 58744b575..b34a36492 100644
--- a/plugins/firstorder/formula.ml
+++ b/plugins/firstorder/formula.ml
@@ -15,7 +15,8 @@ open Tacmach
open Util
open Declarations
open Globnames
-open Context.Rel.Declaration
+
+module RelDecl = Context.Rel.Declaration
let qflag=ref true
@@ -141,7 +142,7 @@ let build_atoms gl metagen side cciterm =
end;
let v = ind_hyps 0 i l gl in
let g i _ decl =
- build_rec env polarity (lift i (get_type decl)) in
+ build_rec env polarity (lift i (RelDecl.get_type decl)) in
let f l =
List.fold_left_i g (1-(List.length l)) () l in
if polarity && (* we have a constant constructor *)
@@ -152,7 +153,7 @@ let build_atoms gl metagen side cciterm =
let var=mkMeta (metagen true) in
let v =(ind_hyps 1 i l gl).(0) in
let g i _ decl =
- build_rec (var::env) polarity (lift i (get_type decl)) in
+ build_rec (var::env) polarity (lift i (RelDecl.get_type decl)) in
List.fold_left_i g (2-(List.length l)) () v
| Forall(_,b)->
let var=mkMeta (metagen true) in
@@ -225,7 +226,7 @@ let build_formula side nam typ gl metagen=
| And(_,_,_) -> Rand
| Or(_,_,_) -> Ror
| Exists (i,l) ->
- let d = get_type (List.last (ind_hyps 0 i l gl).(0)) in
+ let d = RelDecl.get_type (List.last (ind_hyps 0 i l gl).(0)) in
Rexists(m,d,trivial)
| Forall (_,a) -> Rforall
| Arrow (a,b) -> Rarrow in