diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eauto.ml4 | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 4 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 6 |
3 files changed, 6 insertions, 6 deletions
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4 index f1297647ce..caebb76d4c 100644 --- a/tactics/eauto.ml4 +++ b/tactics/eauto.ml4 @@ -538,7 +538,7 @@ TACTIC EXTEND autounfold_one TACTIC EXTEND autounfoldify | [ "autounfoldify" constr(x) ] -> [ let db = match kind_of_term x with - | Const c -> string_of_label (con_label c) + | Const c -> Label.to_string (con_label c) | _ -> assert false in autounfold ["core";db] onConcl ] END diff --git a/tactics/equality.ml b/tactics/equality.ml index 16ee05f9ec..7ca1116baf 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -253,14 +253,14 @@ let find_elim hdcncl lft2rgt dep cls args gl = | Some false, Some _ -> let c1 = destConst pr1 in let mp,dp,l = repr_con (constant_of_kn (canonical_con c1)) in - let l' = label_of_id (add_suffix (id_of_label l) "_r") 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 begin try let _ = Global.lookup_constant c1' in mkConst c1' with Not_found -> - let rwr_thm = string_of_label l' in + let rwr_thm = Label.to_string l' in error ("Cannot find rewrite principle "^rwr_thm^".") end | _ -> pr1 diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 0f2ac6cfe3..93b39583be 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -127,7 +127,7 @@ let _ = let lookup_atomic id = Id.Map.find id !atomic_mactab let is_atomic_kn kn = let (_,_,l) = repr_kn kn in - Id.Map.mem (id_of_label l) !atomic_mactab + Id.Map.mem (Label.to_id l) !atomic_mactab (* Tactics table (TacExtend). *) @@ -875,7 +875,7 @@ let load_md i ((sp,kn),(local,defs)) = match id with | NewTac id -> let sp = Libnames.make_path dp id in - let kn = Names.make_kn mp dir (label_of_id id) in + let kn = Names.make_kn mp dir (Label.of_id id) in Nametab.push_tactic (Until i) sp kn; add (kn,t) | UpdateTac kn -> replace (kn,t)) defs @@ -887,7 +887,7 @@ let open_md i ((sp,kn),(local,defs)) = match id with NewTac id -> let sp = Libnames.make_path dp id in - let kn = Names.make_kn mp dir (label_of_id id) in + let kn = Names.make_kn mp dir (Label.of_id id) in Nametab.push_tactic (Exactly i) sp kn | UpdateTac kn -> ()) defs |