diff options
Diffstat (limited to 'tactics/equality.ml')
| -rw-r--r-- | tactics/equality.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/tactics/equality.ml b/tactics/equality.ml index 8d457d9f4..1af172bfb 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -399,7 +399,7 @@ let general_multi_rewrite l2r with_evars ?tac c cl = (* If the term to rewrite uses an hypothesis H, don't rewrite in H *) let ids = let ids_in_c = Environ.global_vars_set (Global.env()) (fst c) in - Idset.fold (fun id l -> List.remove id l) ids_in_c (pf_ids_of_hyps gl) + Id.Set.fold (fun id l -> List.remove id l) ids_in_c (pf_ids_of_hyps gl) in do_hyps_atleastonce ids gl in if cl.concl_occs == NoOccurrences then do_hyps else @@ -755,7 +755,7 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq = let eq_elim = ind_scheme_of_eq lbeq in (applist (eq_elim, [t;t1;mkNamedLambda e t discriminator;i;t2]), absurd_term) -let eq_baseid = id_of_string "e" +let eq_baseid = Id.of_string "e" let apply_on_clause (f,t) clause = let sigma = clause.evd in @@ -1140,7 +1140,7 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause = then ( (* Require Import Eqdec_dec copied from vernac_require in vernacentries.ml*) let qidl = qualid_of_reference - (Ident (Loc.ghost,id_of_string "Eqdep_dec")) in + (Ident (Loc.ghost,Id.of_string "Eqdep_dec")) in Library.require_library [qidl] (Some false); (* cut with the good equality and prove the requested goal *) tclTHENS (cut (mkApp (ceq,new_eq_args)) ) @@ -1394,7 +1394,7 @@ let restrict_to_eq_and_identity eq = (* compatibility *) not (eq_constr eq (constr_of_global glob_identity)) then raise PatternMatchingFailure -exception FoundHyp of (identifier * constr * bool) +exception FoundHyp of (Id.t * constr * bool) (* tests whether hyp [c] is [x = t] or [t = x], [x] not occuring in [t] *) let is_eq_x gl x (id,_,c) = @@ -1412,7 +1412,7 @@ let subst_one dep_proof_ok x (hyp,rhs,dir) gl = (* The set of hypotheses using x *) let depdecls = let test (id,_,c as dcl) = - if not (id_eq id hyp) && occur_var_in_decl (pf_env gl) x dcl then Some dcl + if not (Id.equal id hyp) && occur_var_in_decl (pf_env gl) x dcl then Some dcl else None in List.rev (List.map_filter test (pf_hyps gl)) in let dephyps = List.map (fun (id,_,_) -> id) depdecls in |