From 81107b12644c78f204d0a46df520b8b2d8e72142 Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Thu, 26 Apr 2018 14:25:30 +0200 Subject: Deprecate Evarconv.e_conv,e_cumul --- tactics/tactics.ml | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) (limited to 'tactics/tactics.ml') diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 66505edb5..60070e6fe 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -3813,7 +3813,10 @@ let specialize_eqs id = let ty = Tacmach.New.pf_get_hyp_typ id gl in let evars = ref (Proofview.Goal.sigma gl) in let unif env evars c1 c2 = - compare_upto_variables !evars c1 c2 && Evarconv.e_conv env evars c1 c2 + compare_upto_variables !evars c1 c2 && + (match Evarconv.conv env !evars c1 c2 with + | Some sigma -> evars := sigma; true + | None -> false) in let rec aux in_eqs ctx acc ty = match EConstr.kind !evars ty with @@ -4366,7 +4369,7 @@ let check_expected_type env sigma (elimc,bl) elimt = let sigma,cl = make_evar_clause env sigma ~len:(n - 1) elimt in let sigma = solve_evar_clause env sigma true cl bl in let (_,u,_) = destProd sigma cl.cl_concl in - fun t -> Evarconv.e_cumul env (ref sigma) t u + fun t -> Option.has_some (Evarconv.cumul env sigma t u) let check_enough_applied env sigma elim = (* A heuristic to decide whether the induction arg is enough applied *) -- cgit v1.2.3