aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/firstorder
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/firstorder')
-rw-r--r--plugins/firstorder/instances.ml3
-rw-r--r--plugins/firstorder/rules.ml2
2 files changed, 2 insertions, 3 deletions
diff --git a/plugins/firstorder/instances.ml b/plugins/firstorder/instances.ml
index ef8172de4..9dc2a51a6 100644
--- a/plugins/firstorder/instances.ml
+++ b/plugins/firstorder/instances.ml
@@ -117,10 +117,9 @@ let mk_open_instance id idc gl m t=
let nid=(fresh_id avoid var_id gl) in
let evmap = Sigma.Unsafe.of_evar_map evmap in
let Sigma ((c, _), evmap, _) = Evarutil.new_type_evar env evmap Evd.univ_flexible in
- let c = EConstr.Unsafe.to_constr c in
let evmap = Sigma.to_evar_map evmap in
let decl = LocalAssum (Name nid, c) in
- aux (n-1) (nid::avoid) (Environ.push_rel decl env) evmap (decl::decls) in
+ aux (n-1) (nid::avoid) (EConstr.push_rel decl env) evmap (decl::decls) in
let evmap, decls = aux m [] env evmap [] in
evmap, decls, revt
diff --git a/plugins/firstorder/rules.ml b/plugins/firstorder/rules.ml
index 36bd91ab6..a60fd4d8f 100644
--- a/plugins/firstorder/rules.ml
+++ b/plugins/firstorder/rules.ml
@@ -42,7 +42,7 @@ let wrap n b continue seq 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
+ add_formula Hyp (VarRef id) (EConstr.Unsafe.to_constr (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 (EConstr.Unsafe.to_constr (pf_concl gls)) seq1 gls else seq1 in