diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 7c03a3ba6a..c36ad980ef 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -374,16 +374,16 @@ let find_elim hdcncl lft2rgt dep cls ot = | Some true, None | Some false, Some _ -> let c1 = destConstRef pr1 in - let mp,dp,l = repr_con (constant_of_kn (canonical_con c1)) in + let mp,dp,l = Constant.repr3 (Constant.make1 (Constant.canonical c1)) in let l' = Label.of_id (add_suffix (Label.to_id l) "_r") in - let c1' = Global.constant_of_delta_kn (make_kn mp dp l') in + let c1' = Global.constant_of_delta_kn (KerName.make mp dp l') in begin try let _ = Global.lookup_constant c1' in c1' with Not_found -> user_err ~hdr:"Equality.find_elim" - (str "Cannot find rewrite principle " ++ pr_label l' ++ str ".") + (str "Cannot find rewrite principle " ++ Label.print l' ++ str ".") end | _ -> destConstRef pr1 end @@ -1760,7 +1760,7 @@ let subst_one_var dep_proof_ok x = let test hyp _ = is_eq_x gl x hyp in Context.Named.fold_outside test ~init:() hyps; user_err ~hdr:"Subst" - (str "Cannot find any non-recursive equality over " ++ pr_id x ++ + (str "Cannot find any non-recursive equality over " ++ Id.print x ++ str".") with FoundHyp res -> res in subst_one dep_proof_ok x res @@ -1824,9 +1824,9 @@ let subst_all ?(flags=default_subst_tactic_flags) () = (* J.F.: added to prevent failure on goal containing x=x as an hyp *) if EConstr.eq_constr sigma x y then Proofview.tclUNIT () else match EConstr.kind sigma x, EConstr.kind sigma y with - | Var x', _ when not (occur_term sigma x y) && not (is_evaluable env (EvalVarRef x')) -> + | Var x', _ when not (dependent sigma x y) && not (is_evaluable env (EvalVarRef x')) -> subst_one flags.rewrite_dependent_proof x' (hyp,y,true) - | _, Var y' when not (occur_term sigma y x) && not (is_evaluable env (EvalVarRef y')) -> + | _, Var y' when not (dependent sigma y x) && not (is_evaluable env (EvalVarRef y')) -> subst_one flags.rewrite_dependent_proof y' (hyp,x,false) | _ -> Proofview.tclUNIT () |