diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/eauto.ml | 2 | ||||
| -rw-r--r-- | tactics/equality.ml | 6 | ||||
| -rw-r--r-- | tactics/ind_tables.ml | 4 | ||||
| -rw-r--r-- | tactics/ind_tables.mli | 8 | ||||
| -rw-r--r-- | tactics/tacticals.ml | 4 | ||||
| -rw-r--r-- | tactics/tacticals.mli | 16 | ||||
| -rw-r--r-- | tactics/tactics.ml | 6 | ||||
| -rw-r--r-- | tactics/tactics.mli | 6 |
8 files changed, 26 insertions, 26 deletions
diff --git a/tactics/eauto.ml b/tactics/eauto.ml index 2b5bbfcd1b..9097aebd01 100644 --- a/tactics/eauto.ml +++ b/tactics/eauto.ml @@ -439,7 +439,7 @@ let autounfolds db occs cls gl = in let (ids, csts) = Hint_db.unfolds db in let hyps = pf_ids_of_hyps gl in - let ids = Idset.filter (fun id -> List.mem id hyps) ids in + let ids = Id.Set.filter (fun id -> List.mem id hyps) ids in Cset.fold (fun cst -> cons (AllOccurrences, EvalConstRef cst)) csts (Id.Set.fold (fun id -> cons (AllOccurrences, EvalVarRef id)) ids [])) db) in Proofview.V82.of_tactic (unfold_option unfolds cls) gl diff --git a/tactics/equality.ml b/tactics/equality.ml index 7c03a3ba6a..881000219c 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 diff --git a/tactics/ind_tables.ml b/tactics/ind_tables.ml index 7f087ea01a..240b5a7e0f 100644 --- a/tactics/ind_tables.ml +++ b/tactics/ind_tables.ml @@ -29,7 +29,7 @@ open Pp (* Registering schemes in the environment *) type mutual_scheme_object_function = - internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants + internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants type individual_scheme_object_function = internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants @@ -57,7 +57,7 @@ let discharge_scheme (_,(kind,l)) = Some (kind,Array.map (fun (ind,const) -> (Lib.discharge_inductive ind,Lib.discharge_con const)) l) -let inScheme : string * (inductive * constant) array -> obj = +let inScheme : string * (inductive * Constant.t) array -> obj = declare_object {(default_object "SCHEME") with cache_function = cache_scheme; load_function = (fun _ -> cache_scheme); diff --git a/tactics/ind_tables.mli b/tactics/ind_tables.mli index f825c4f4a3..232a193ac3 100644 --- a/tactics/ind_tables.mli +++ b/tactics/ind_tables.mli @@ -20,7 +20,7 @@ type individual type 'a scheme_kind type mutual_scheme_object_function = - internal_flag -> mutual_inductive -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants + internal_flag -> MutInd.t -> constr array Evd.in_evar_universe_context * Safe_typing.private_constants type individual_scheme_object_function = internal_flag -> inductive -> constr Evd.in_evar_universe_context * Safe_typing.private_constants @@ -37,13 +37,13 @@ val declare_individual_scheme_object : string -> ?aux:string -> val define_individual_scheme : individual scheme_kind -> internal_flag (** internal *) -> - Id.t option -> inductive -> constant * Safe_typing.private_constants + Id.t option -> inductive -> Constant.t * Safe_typing.private_constants val define_mutual_scheme : mutual scheme_kind -> internal_flag (** internal *) -> - (int * Id.t) list -> mutual_inductive -> constant array * Safe_typing.private_constants + (int * Id.t) list -> MutInd.t -> Constant.t array * Safe_typing.private_constants (** Main function to retrieve a scheme in the cache or to generate it *) -val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> constant * Safe_typing.private_constants +val find_scheme : ?mode:internal_flag -> 'a scheme_kind -> inductive -> Constant.t * Safe_typing.private_constants val check_scheme : 'a scheme_kind -> inductive -> bool diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml index bce0dda10c..fe733899f5 100644 --- a/tactics/tacticals.ml +++ b/tactics/tacticals.ml @@ -622,8 +622,8 @@ module New = struct | _ -> let name_elim = match EConstr.kind sigma elim with - | Const (kn, _) -> string_of_con kn - | Var id -> string_of_id id + | Const (kn, _) -> Constant.to_string kn + | Var id -> Id.to_string id | _ -> "\b" in user_err ~hdr:"Tacticals.general_elim_then_using" diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli index 2a04c413be..3abd42d46a 100644 --- a/tactics/tacticals.mli +++ b/tactics/tacticals.mli @@ -226,12 +226,12 @@ module New : sig val nLastDecls : 'a Proofview.Goal.t -> int -> named_context - val ifOnHyp : (identifier * types -> bool) -> - (identifier -> unit Proofview.tactic) -> (identifier -> unit Proofview.tactic) -> - identifier -> unit Proofview.tactic + val ifOnHyp : (Id.t * types -> bool) -> + (Id.t -> unit Proofview.tactic) -> (Id.t -> unit Proofview.tactic) -> + Id.t -> unit Proofview.tactic - val onNthHypId : int -> (identifier -> unit tactic) -> unit tactic - val onLastHypId : (identifier -> unit tactic) -> unit tactic + val onNthHypId : int -> (Id.t -> unit tactic) -> unit tactic + val onLastHypId : (Id.t -> unit tactic) -> unit tactic val onLastHyp : (constr -> unit tactic) -> unit tactic val onLastDecl : (named_declaration -> unit tactic) -> unit tactic @@ -239,9 +239,9 @@ module New : sig (named_context -> unit tactic) -> unit tactic val afterHyp : Id.t -> (named_context -> unit tactic) -> unit tactic - val tryAllHyps : (identifier -> unit tactic) -> unit tactic - val tryAllHypsAndConcl : (identifier option -> unit tactic) -> unit tactic - val onClause : (identifier option -> unit tactic) -> clause -> unit tactic + val tryAllHyps : (Id.t -> unit tactic) -> unit tactic + val tryAllHypsAndConcl : (Id.t option -> unit tactic) -> unit tactic + val onClause : (Id.t option -> unit tactic) -> clause -> unit tactic val elimination_sort_of_goal : 'a Proofview.Goal.t -> sorts_family val elimination_sort_of_hyp : Id.t -> 'a Proofview.Goal.t -> sorts_family diff --git a/tactics/tactics.ml b/tactics/tactics.ml index f8f9e029b6..866daa904d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -580,7 +580,7 @@ let mutual_fix f n rest j = Proofview.Goal.enter begin fun gl -> | (f, n, ar) :: oth -> let open Context.Named.Declaration in let (sp', u') = check_mutind env sigma n ar in - if not (eq_mind sp sp') then + if not (MutInd.equal sp sp') then error "Fixpoints should be on the same mutual inductive declaration."; if mem_named_context_val f sign then user_err ~hdr:"Logic.prim_refiner" @@ -1376,7 +1376,7 @@ let enforce_prop_bound_names rename tac = (* "very_standard" says that we should have "H" names only, but this would break compatibility even more... *) let s = match Namegen.head_name sigma t with - | Some id when not very_standard -> string_of_id id + | Some id when not very_standard -> Id.to_string id | _ -> "" in Name (add_suffix Namegen.default_prop_ident s) else @@ -1607,7 +1607,7 @@ let general_elim_clause with_evars flags id c e = (* Apply a tactic below the products of the conclusion of a lemma *) type conjunction_status = - | DefinedRecord of constant option list + | DefinedRecord of Constant.t option list | NotADefinedRecordUseScheme of constr let make_projection env sigma params cstr sign elim i n c u = diff --git a/tactics/tactics.mli b/tactics/tactics.mli index 32923ea811..98cf1b4373 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -271,7 +271,7 @@ type eliminator = { val general_elim : evars_flag -> clear_flag -> constr with_bindings -> eliminator -> unit Proofview.tactic -val general_elim_clause : evars_flag -> unify_flags -> identifier option -> +val general_elim_clause : evars_flag -> unify_flags -> Id.t option -> clausenv -> eliminator -> unit Proofview.tactic val default_elim : evars_flag -> clear_flag -> constr with_bindings -> @@ -355,7 +355,7 @@ val assert_before : Name.t -> types -> unit Proofview.tactic val assert_after : Name.t -> types -> unit Proofview.tactic val assert_as : (* true = before *) bool -> - (* optionally tell if a specialization of some hyp: *) identifier option -> + (* optionally tell if a specialization of some hyp: *) Id.t option -> intro_pattern option -> constr -> unit Proofview.tactic (** Implements the tactics assert, enough and pose proof; note that "by" @@ -428,7 +428,7 @@ module Simple : sig val eapply : constr -> unit Proofview.tactic val elim : constr -> unit Proofview.tactic val case : constr -> unit Proofview.tactic - val apply_in : identifier -> constr -> unit Proofview.tactic + val apply_in : Id.t -> constr -> unit Proofview.tactic end |