aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/instances.ml2
-rw-r--r--plugins/firstorder/rules.ml4
-rw-r--r--plugins/firstorder/sequent.ml2
3 files changed, 5 insertions, 3 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index 24d4346d9..2881b5333 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -107,7 +107,7 @@ let mk_open_instance id idc gl m t=
let typ=pf_unsafe_type_of gl (EConstr.of_constr idc) in
(* since we know we will get a product,
reduction is not too expensive *)
- let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap (EConstr.of_constr typ))) in
+ let (nam,_,_)=destProd (EConstr.Unsafe.to_constr (whd_all env evmap typ)) in
match nam with
Name id -> id
| Anonymous -> dummy_bvid in
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index bed7a727f..38dae0b20 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -38,14 +38,14 @@ let wrap n b continue seq gls=
[]->anomaly (Pp.str "Not the expected number of hyps")
| nd::q->
let id = NamedDecl.get_id nd in
- if occur_var env (project gls) id (EConstr.of_constr (pf_concl gls)) ||
+ if occur_var env (project gls) id (pf_concl gls) ||
List.exists (occur_var_in_decl env (project gls) id) ctx then
(aux (i-1) q (nd::ctx))
else
add_formula Hyp (VarRef id) (NamedDecl.get_type nd) (aux (i-1) q (nd::ctx)) gls in
let seq1=aux n nc [] in
let seq2=if b then
- add_formula Concl dummy_id (pf_concl gls) seq1 gls else seq1 in
+ add_formula Concl dummy_id (EConstr.Unsafe.to_constr (pf_concl gls)) seq1 gls else seq1 in
continue seq2 gls
let basename_of_global=function
diff --git a/plugins/firstorder/sequent.ml b/plugins/firstorder/sequent.ml
index 91cd102a2..fb0c22c2b 100644
--- a/plugins/firstorder/sequent.ml
+++ b/plugins/firstorder/sequent.ml
@@ -201,6 +201,7 @@ let extend_with_ref_list l seq gl =
let f gr (seq,gl) =
let gl, c = pf_eapply Evd.fresh_global gl gr in
let typ=(pf_unsafe_type_of gl (EConstr.of_constr c)) in
+ let typ = EConstr.Unsafe.to_constr typ in
(add_formula Hyp gr typ seq gl,gl) in
List.fold_right f l (seq,gl)
@@ -216,6 +217,7 @@ let extend_with_auto_hints l seq gl=
(try
let (gr, _) = Termops.global_of_constr (project gl) c in
let typ=(pf_unsafe_type_of gl c) in
+ let typ = EConstr.Unsafe.to_constr typ in
seqref:=add_formula Hint gr typ !seqref gl
with Not_found->())
| _-> () in