aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/setoid_ring
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/setoid_ring')
-rw-r--r--plugins/setoid_ring/newring.ml8
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml
index e1b95ddbc..b0a3e839b 100644
--- a/plugins/setoid_ring/newring.ml
+++ b/plugins/setoid_ring/newring.ml
@@ -493,8 +493,8 @@ let ring_equality env evd (r,add,mul,opp,req) =
match opp with
Some opp -> plapp evd coq_eq_morph [|r;add;mul;opp|]
| None -> plapp evd coq_eq_smorph [|r;add;mul|] in
- let setoid = Typing.e_solve_evars env evd setoid in
- let op_morph = Typing.e_solve_evars env evd op_morph in
+ let setoid = Typing.e_solve_evars env evd (EConstr.of_constr setoid) in
+ let op_morph = Typing.e_solve_evars env evd (EConstr.of_constr op_morph) in
(setoid,op_morph)
| _ ->
let setoid = setoid_of_relation (Global.env ()) evd r req in
@@ -581,7 +581,7 @@ let make_hyp_list env evd lH =
(fun c l -> plapp evd coq_cons [|carrier; (make_hyp env evd c); l|]) lH
(plapp evd coq_nil [|carrier|])
in
- let l' = Typing.e_solve_evars env evd l in
+ let l' = Typing.e_solve_evars env evd (EConstr.of_constr l) in
Evarutil.nf_evars_universes !evd l'
let interp_power env evd pow =
@@ -707,7 +707,7 @@ let make_term_list env evd carrier rl =
let l = List.fold_right
(fun x l -> plapp evd coq_cons [|carrier;x;l|]) rl
(plapp evd coq_nil [|carrier|])
- in Typing.e_solve_evars env evd l
+ in Typing.e_solve_evars env evd (EConstr.of_constr l)
let carg = Tacinterp.Value.of_constr
let tacarg expr =