From e27949240f5b1ee212e7d0fe3326a21a13c4abb0 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Sun, 6 Nov 2016 17:21:44 +0100 Subject: Typing API using EConstr. --- plugins/setoid_ring/newring.ml | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) (limited to 'plugins/setoid_ring') 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 = -- cgit v1.2.3