diff options
| author | Pierre-Marie Pédrot | 2016-02-15 13:31:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-02-15 13:41:16 +0100 |
| commit | 1a8c37ca352c95b4cd530efbbf47f0e7671d1fb3 (patch) | |
| tree | 15aadd829fe3e8c3ee0a747de34a9b96614bfdba /plugins/setoid_ring | |
| parent | 968dfdb15cc11d48783017b2a91147b25c854ad6 (diff) | |
Renaming functions in Typing to stick to the standard e_* scheme.
Diffstat (limited to 'plugins/setoid_ring')
| -rw-r--r-- | plugins/setoid_ring/newring.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/plugins/setoid_ring/newring.ml b/plugins/setoid_ring/newring.ml index e203b9f651..ed6db90d63 100644 --- a/plugins/setoid_ring/newring.ml +++ b/plugins/setoid_ring/newring.ml @@ -527,8 +527,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.solve_evars env evd setoid in - let op_morph = Typing.solve_evars env evd op_morph in + let setoid = Typing.e_solve_evars env evd setoid in + let op_morph = Typing.e_solve_evars env evd op_morph in (setoid,op_morph) | _ -> let setoid = setoid_of_relation (Global.env ()) evd r req in @@ -627,7 +627,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.solve_evars env evd l in + let l' = Typing.e_solve_evars env evd l in Evarutil.nf_evars_universes !evd l' let interp_power env evd pow = @@ -753,7 +753,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.solve_evars env evd l + in Typing.e_solve_evars env evd l let carg = Tacinterp.Value.of_constr let tacarg expr = |