aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/ltac
diff options
context:
space:
mode:
Diffstat (limited to 'plugins/ltac')
-rw-r--r--plugins/ltac/coretactics.ml46
-rw-r--r--plugins/ltac/evar_tactics.ml11
-rw-r--r--plugins/ltac/extraargs.ml48
-rw-r--r--plugins/ltac/extratactics.ml48
-rw-r--r--plugins/ltac/g_auto.ml41
-rw-r--r--plugins/ltac/g_class.ml41
-rw-r--r--plugins/ltac/g_eqdecide.ml41
-rw-r--r--plugins/ltac/g_ltac.ml418
-rw-r--r--plugins/ltac/g_tactic.ml410
-rw-r--r--plugins/ltac/pptactic.ml6
-rw-r--r--plugins/ltac/profile_ltac.ml2
-rw-r--r--plugins/ltac/rewrite.ml10
-rw-r--r--plugins/ltac/rewrite.mli3
-rw-r--r--plugins/ltac/taccoerce.ml4
-rw-r--r--plugins/ltac/tacentries.ml6
-rw-r--r--plugins/ltac/tacinterp.ml22
-rw-r--r--plugins/ltac/tactic_debug.ml10
-rw-r--r--plugins/ltac/tauto.ml2
18 files changed, 61 insertions, 68 deletions
diff --git a/plugins/ltac/coretactics.ml4 b/plugins/ltac/coretactics.ml4
index 63057c3ae..07b8746fb 100644
--- a/plugins/ltac/coretactics.ml4
+++ b/plugins/ltac/coretactics.ml4
@@ -10,12 +10,12 @@
open API
open Util
-open Names
open Locus
open Misctypes
open Genredexpr
open Stdarg
open Extraargs
+open Names
DECLARE PLUGIN "coretactics"
@@ -307,7 +307,7 @@ let initial_atomic () =
let nocl = {onhyps=Some[];concl_occs=AllOccurrences} in
let iter (s, t) =
let body = TacAtom (Loc.tag t) in
- Tacenv.register_ltac false false (Id.of_string s) body
+ Tacenv.register_ltac false false (Names.Id.of_string s) body
in
let () = List.iter iter
[ "red", TacReduce(Red false,nocl);
@@ -317,7 +317,7 @@ let initial_atomic () =
"intros", TacIntroPattern (false,[]);
]
in
- let iter (s, t) = Tacenv.register_ltac false false (Id.of_string s) t in
+ let iter (s, t) = Tacenv.register_ltac false false (Names.Id.of_string s) t in
List.iter iter
[ "idtac",TacId [];
"fail", TacFail(TacLocal,ArgArg 0,[]);
diff --git a/plugins/ltac/evar_tactics.ml b/plugins/ltac/evar_tactics.ml
index 958f43bd7..a299e11f8 100644
--- a/plugins/ltac/evar_tactics.ml
+++ b/plugins/ltac/evar_tactics.ml
@@ -87,16 +87,16 @@ let let_evar name typ =
let _ = Typing.e_sort_of env sigma typ in
let sigma = !sigma in
let id = match name with
- | Names.Anonymous ->
+ | Name.Anonymous ->
let id = Namegen.id_of_name_using_hdchar env sigma typ name in
Namegen.next_ident_away_in_goal id (Termops.ids_of_named_context (Environ.named_context env))
- | Names.Name id -> id
+ | Name.Name id -> id
in
let (sigma, evar) = Evarutil.new_evar env sigma ~src ~naming:(Misctypes.IntroFresh id) typ in
Tacticals.New.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
- (Tactics.letin_tac None (Names.Name id) evar None Locusops.nowhere)
+ (Tactics.letin_tac None (Name.Name id) evar None Locusops.nowhere)
end
-
+
let hget_evar n =
let open EConstr in
Proofview.Goal.nf_enter begin fun gl ->
@@ -108,6 +108,5 @@ let hget_evar n =
if n <= 0 then user_err Pp.(str "Incorrect existential variable index.");
let ev = List.nth evl (n-1) in
let ev_type = EConstr.existential_type sigma ev in
- Tactics.change_concl (mkLetIn (Anonymous,mkEvar ev,ev_type,concl))
+ Tactics.change_concl (mkLetIn (Name.Anonymous,mkEvar ev,ev_type,concl))
end
-
diff --git a/plugins/ltac/extraargs.ml4 b/plugins/ltac/extraargs.ml4
index b26fd78ef..44f33ab80 100644
--- a/plugins/ltac/extraargs.ml4
+++ b/plugins/ltac/extraargs.ml4
@@ -85,7 +85,7 @@ let pr_int_list_full _prc _prlc _prt l = pr_int_list l
let pr_occurrences _prc _prlc _prt l =
match l with
| ArgArg x -> pr_int_list x
- | ArgVar (loc, id) -> Nameops.pr_id id
+ | ArgVar (loc, id) -> Id.print id
let occurrences_of = function
| [] -> NoOccurrences
@@ -201,8 +201,8 @@ let pr_gen_place pr_id = function
| HypLocation (id,InHypValueOnly) ->
str "in (Value of " ++ pr_id id ++ str ")"
-let pr_loc_place _ _ _ = pr_gen_place (fun (_,id) -> Nameops.pr_id id)
-let pr_place _ _ _ = pr_gen_place Nameops.pr_id
+let pr_loc_place _ _ _ = pr_gen_place (fun (_,id) -> Id.print id)
+let pr_place _ _ _ = pr_gen_place Id.print
let pr_hloc = pr_loc_place () () ()
let intern_place ist = function
@@ -238,7 +238,7 @@ ARGUMENT EXTEND hloc
END
-let pr_rename _ _ _ (n, m) = Nameops.pr_id n ++ str " into " ++ Nameops.pr_id m
+let pr_rename _ _ _ (n, m) = Id.print n ++ str " into " ++ Id.print m
ARGUMENT EXTEND rename
TYPED AS ident * ident
diff --git a/plugins/ltac/extratactics.ml4 b/plugins/ltac/extratactics.ml4
index 9f53c44a4..18d7b818c 100644
--- a/plugins/ltac/extratactics.ml4
+++ b/plugins/ltac/extratactics.ml4
@@ -464,8 +464,8 @@ open Evar_tactics
(* TODO: add support for some test similar to g_constr.name_colon so that
expressions like "evar (list A)" do not raise a syntax error *)
TACTIC EXTEND evar
- [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name id) typ ]
-| [ "evar" constr(typ) ] -> [ let_evar Anonymous typ ]
+ [ "evar" test_lpar_id_colon "(" ident(id) ":" lconstr(typ) ")" ] -> [ let_evar (Name.Name id) typ ]
+| [ "evar" constr(typ) ] -> [ let_evar Name.Anonymous typ ]
END
TACTIC EXTEND instantiate
@@ -516,7 +516,7 @@ let cache_transitivity_lemma (_,(left,lem)) =
let subst_transitivity_lemma (subst,(b,ref)) = (b,subst_mps subst ref)
-let inTransitivity : bool * Constr.constr -> obj =
+let inTransitivity : bool * Term.constr -> obj =
declare_object {(default_object "TRANSITIVITY-STEPS") with
cache_function = cache_transitivity_lemma;
open_function = (fun i o -> if Int.equal i 1 then cache_transitivity_lemma o);
@@ -684,7 +684,7 @@ let hResolve id c occ t =
let sigma = Evd.merge_universe_context sigma ctx in
let t_constr_type = Retyping.get_type_of env sigma t_constr in
Proofview.tclTHEN (Proofview.Unsafe.tclEVARS sigma)
- (change_concl (mkLetIn (Anonymous,t_constr,t_constr_type,concl)))
+ (change_concl (mkLetIn (Name.Anonymous,t_constr,t_constr_type,concl)))
end
let hResolve_auto id c t =
diff --git a/plugins/ltac/g_auto.ml4 b/plugins/ltac/g_auto.ml4
index 68b63f02c..dfd8e88a9 100644
--- a/plugins/ltac/g_auto.ml4
+++ b/plugins/ltac/g_auto.ml4
@@ -17,7 +17,6 @@ open Pcoq.Prim
open Pcoq.Constr
open Pltac
open Hints
-open Names
DECLARE PLUGIN "g_auto"
diff --git a/plugins/ltac/g_class.ml4 b/plugins/ltac/g_class.ml4
index 3d7d5e3fe..905cfd02a 100644
--- a/plugins/ltac/g_class.ml4
+++ b/plugins/ltac/g_class.ml4
@@ -12,7 +12,6 @@ open API
open Class_tactics
open Stdarg
open Tacarg
-open Names
DECLARE PLUGIN "g_class"
diff --git a/plugins/ltac/g_eqdecide.ml4 b/plugins/ltac/g_eqdecide.ml4
index e91e25111..570cd4e69 100644
--- a/plugins/ltac/g_eqdecide.ml4
+++ b/plugins/ltac/g_eqdecide.ml4
@@ -16,7 +16,6 @@
open API
open Eqdecide
-open Names
DECLARE PLUGIN "g_eqdecide"
diff --git a/plugins/ltac/g_ltac.ml4 b/plugins/ltac/g_ltac.ml4
index 7855fbcfc..4bab31b85 100644
--- a/plugins/ltac/g_ltac.ml4
+++ b/plugins/ltac/g_ltac.ml4
@@ -231,8 +231,8 @@ GEXTEND Gram
| "multimatch" -> General ] ]
;
input_fun:
- [ [ "_" -> Anonymous
- | l = ident -> Name l ] ]
+ [ [ "_" -> Name.Anonymous
+ | l = ident -> Name.Name l ] ]
;
let_clause:
[ [ id = identref; ":="; te = tactic_expr ->
@@ -399,7 +399,7 @@ let pr_ltac_selector = function
| SelectNth i -> int i ++ str ":"
| SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++
str "]" ++ str ":"
-| SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":"
+| SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":"
| SelectAll -> str "all" ++ str ":"
VERNAC ARGUMENT EXTEND ltac_selector PRINTED BY pr_ltac_selector
@@ -469,14 +469,14 @@ let pr_ltac_production_item = function
| None -> mt ()
| Some sep -> str "," ++ spc () ++ quote (str sep)
in
- str arg ++ str "(" ++ Nameops.pr_id id ++ sep ++ str ")"
+ str arg ++ str "(" ++ Id.print id ++ sep ++ str ")"
VERNAC ARGUMENT EXTEND ltac_production_item PRINTED BY pr_ltac_production_item
| [ string(s) ] -> [ Tacentries.TacTerm s ]
| [ ident(nt) "(" ident(p) ltac_production_sep_opt(sep) ")" ] ->
- [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, sep), Some p)) ]
+ [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, sep), Some p)) ]
| [ ident(nt) ] ->
- [ Tacentries.TacNonTerm (Loc.tag ~loc ((Names.Id.to_string nt, None), None)) ]
+ [ Tacentries.TacNonTerm (Loc.tag ~loc ((Id.to_string nt, None), None)) ]
END
VERNAC COMMAND EXTEND VernacTacticNotation
@@ -499,7 +499,7 @@ let pr_ltac_ref = Libnames.pr_reference
let pr_tacdef_body tacdef_body =
let id, redef, body =
match tacdef_body with
- | TacticDefinition ((_,id), body) -> Nameops.pr_id id, false, body
+ | TacticDefinition ((_,id), body) -> Id.print id, false, body
| TacticRedefinition (id, body) -> pr_ltac_ref id, true, body
in
let idl, body =
@@ -507,8 +507,8 @@ let pr_tacdef_body tacdef_body =
| Tacexpr.TacFun (idl,b) -> idl,b
| _ -> [], body in
id ++
- prlist (function Anonymous -> str " _"
- | Name id -> spc () ++ Nameops.pr_id id) idl
+ prlist (function Name.Anonymous -> str " _"
+ | Name.Name id -> spc () ++ Id.print id) idl
++ (if redef then str" ::=" else str" :=") ++ brk(1,1)
++ Pptactic.pr_raw_tactic body
diff --git a/plugins/ltac/g_tactic.ml4 b/plugins/ltac/g_tactic.ml4
index e94cf1c63..a971fc79f 100644
--- a/plugins/ltac/g_tactic.ml4
+++ b/plugins/ltac/g_tactic.ml4
@@ -477,7 +477,7 @@ GEXTEND Gram
| -> None ] ]
;
as_name:
- [ [ "as"; id = ident -> Names.Name id | -> Names.Anonymous ] ]
+ [ [ "as"; id = ident ->Names.Name.Name id | -> Names.Name.Anonymous ] ]
;
by_tactic:
[ [ "by"; tac = tactic_expr LEVEL "3" -> Some tac
@@ -540,7 +540,7 @@ GEXTEND Gram
TacAtom (Loc.tag ~loc:!@loc @@ TacMutualCofix (id,List.map mk_cofix_tac fd))
| IDENT "pose"; (id,b) = bindings_with_parameters ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name id,b,Locusops.nowhere,true,None))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name.Name id,b,Locusops.nowhere,true,None))
| IDENT "pose"; b = constr; na = as_name ->
TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,b,Locusops.nowhere,true,None))
| IDENT "epose"; (id,b) = bindings_with_parameters ->
@@ -548,7 +548,7 @@ GEXTEND Gram
| IDENT "epose"; b = constr; na = as_name ->
TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (true,na,b,Locusops.nowhere,true,None))
| IDENT "set"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name id,c,p,true,None))
+ TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,Names.Name.Name id,c,p,true,None))
| IDENT "set"; c = constr; na = as_name; p = clause_dft_concl ->
TacAtom (Loc.tag ~loc:!@loc @@ TacLetTac (false,na,c,p,true,None))
| IDENT "eset"; (id,c) = bindings_with_parameters; p = clause_dft_concl ->
@@ -600,9 +600,9 @@ GEXTEND Gram
TacAtom (Loc.tag ~loc:!@loc @@ TacAssert (true,false,Some tac,ipat,c))
| IDENT "generalize"; c = constr ->
- TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize [((AllOccurrences,c),Names.Anonymous)])
+ TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize [((AllOccurrences,c),Names.Name.Anonymous)])
| IDENT "generalize"; c = constr; l = LIST1 constr ->
- let gen_everywhere c = ((AllOccurrences,c),Names.Anonymous) in
+ let gen_everywhere c = ((AllOccurrences,c),Names.Name.Anonymous) in
TacAtom (Loc.tag ~loc:!@loc @@ TacGeneralize (List.map gen_everywhere (c::l)))
| IDENT "generalize"; c = constr; lookup_at_as_comma; nl = occs;
na = as_name;
diff --git a/plugins/ltac/pptactic.ml b/plugins/ltac/pptactic.ml
index c84a7c00a..8300a55e3 100644
--- a/plugins/ltac/pptactic.ml
+++ b/plugins/ltac/pptactic.ml
@@ -335,11 +335,11 @@ type 'a extra_genarg_printer =
| ArgVar (loc,id) -> pr_with_comments ?loc (pr_id id)
let pr_ltac_constant kn =
- if !Flags.in_debugger then pr_kn kn
+ if !Flags.in_debugger then KerName.print kn
else try
pr_qualid (Nametab.shortest_qualid_of_tactic kn)
with Not_found -> (* local tactic not accessible anymore *)
- str "<" ++ pr_kn kn ++ str ">"
+ str "<" ++ KerName.print kn ++ str ">"
let pr_evaluable_reference_env env = function
| EvalVarRef id -> pr_id id
@@ -482,7 +482,7 @@ type 'a extra_genarg_printer =
| SelectNth i -> int i ++ str ":"
| SelectList l -> str "[" ++ prlist_with_sep (fun () -> str ", ") pr_range_selector l ++
str "]" ++ str ":"
- | SelectId id -> str "[" ++ Nameops.pr_id id ++ str "]" ++ str ":"
+ | SelectId id -> str "[" ++ Id.print id ++ str "]" ++ str ":"
| SelectAll -> str "all" ++ str ":"
let pr_lazy = function
diff --git a/plugins/ltac/profile_ltac.ml b/plugins/ltac/profile_ltac.ml
index 0fbb9df2d..020b3048f 100644
--- a/plugins/ltac/profile_ltac.ml
+++ b/plugins/ltac/profile_ltac.ml
@@ -247,7 +247,7 @@ let string_of_call ck =
(match ck with
| Tacexpr.LtacNotationCall s -> Pptactic.pr_alias_key s
| Tacexpr.LtacNameCall cst -> Pptactic.pr_ltac_constant cst
- | Tacexpr.LtacVarCall (id, t) -> Nameops.pr_id id
+ | Tacexpr.LtacVarCall (id, t) -> Names.Id.print id
| Tacexpr.LtacAtomCall te ->
(Pptactic.pr_glob_tactic (Global.env ())
(Tacexpr.TacAtom (Loc.tag te)))
diff --git a/plugins/ltac/rewrite.ml b/plugins/ltac/rewrite.ml
index 9069635c1..3927ca7ce 100644
--- a/plugins/ltac/rewrite.ml
+++ b/plugins/ltac/rewrite.ml
@@ -427,7 +427,7 @@ let split_head = function
| [] -> assert(false)
let eq_pb (ty, env, x, y as pb) (ty', env', x', y' as pb') =
- pb == pb' || (ty == ty' && Constr.equal x x' && Constr.equal y y')
+ pb == pb' || (ty == ty' && Term.eq_constr x x' && Term.eq_constr y y')
let problem_inclusion x y =
List.for_all (fun pb -> List.exists (fun pb' -> eq_pb pb pb') y) x
@@ -957,7 +957,7 @@ let fold_match ?(force=false) env sigma c =
let unfold_match env sigma sk app =
match EConstr.kind sigma app with
- | App (f', args) when eq_constant (fst (destConst sigma f')) sk ->
+ | App (f', args) when Constant.equal (fst (destConst sigma f')) sk ->
let v = Environ.constant_value_in (Global.env ()) (sk,Univ.Instance.empty)(*FIXME*) in
let v = EConstr.of_constr v in
Reductionops.whd_beta sigma (mkApp (v, args))
@@ -1371,7 +1371,7 @@ module Strategies =
fail cs
let inj_open hint = (); fun sigma ->
- let ctx = Evd.evar_universe_context_of hint.Autorewrite.rew_ctx in
+ let ctx = UState.of_context_set hint.Autorewrite.rew_ctx in
let sigma = Evd.merge_universe_context sigma ctx in
(sigma, (EConstr.of_constr hint.Autorewrite.rew_lemma, NoBindings))
@@ -1472,7 +1472,7 @@ let cl_rewrite_clause_aux ?(abs=None) strat env avoid sigma concl is_hyp : resul
let evars = (!evdref, Evar.Set.empty) in
let evars, cstr =
let prop, (evars, arrow) =
- if is_prop_sort sort then true, app_poly_sort true env evars impl [||]
+ if Sorts.is_prop sort then true, app_poly_sort true env evars impl [||]
else false, app_poly_sort false env evars TypeGlobal.arrow [||]
in
match is_hyp with
@@ -1965,7 +1965,7 @@ let add_morphism_infer glob m n =
if Lib.is_modtype () then
let cst = Declare.declare_constant ~internal:Declare.InternalTacticRequest instance_id
(Entries.ParameterEntry
- (None,poly,(instance,Evd.evar_context_universe_context uctx),None),
+ (None,poly,(instance,UState.context uctx),None),
Decl_kinds.IsAssumption Decl_kinds.Logical)
in
add_instance (Typeclasses.new_instance
diff --git a/plugins/ltac/rewrite.mli b/plugins/ltac/rewrite.mli
index 77286452b..d7f92fd6e 100644
--- a/plugins/ltac/rewrite.mli
+++ b/plugins/ltac/rewrite.mli
@@ -8,7 +8,6 @@
open API
open Names
-open Constr
open Environ
open EConstr
open Constrexpr
@@ -39,7 +38,7 @@ type ('constr,'redexpr) strategy_ast =
type rewrite_proof =
| RewPrf of constr * constr
- | RewCast of cast_kind
+ | RewCast of Term.cast_kind
type evars = evar_map * Evar.Set.t (* goal evars, constraint evars *)
diff --git a/plugins/ltac/taccoerce.ml b/plugins/ltac/taccoerce.ml
index 14e5aa72a..117a16b0a 100644
--- a/plugins/ltac/taccoerce.ml
+++ b/plugins/ltac/taccoerce.ml
@@ -132,8 +132,8 @@ let coerce_var_to_ident fresh env sigma v =
let coerce_to_ident_not_fresh env sigma v =
let g = sigma in
let id_of_name = function
- | Names.Anonymous -> Id.of_string "x"
- | Names.Name x -> x in
+ | Name.Anonymous -> Id.of_string "x"
+ | Name.Name x -> x in
let v = Value.normalize v in
let fail () = raise (CannotCoerceTo "an identifier") in
if has_type v (topwit wit_intro_pattern) then
diff --git a/plugins/ltac/tacentries.ml b/plugins/ltac/tacentries.ml
index dbc32c2f6..270225e23 100644
--- a/plugins/ltac/tacentries.ml
+++ b/plugins/ltac/tacentries.ml
@@ -419,7 +419,7 @@ let is_defined_tac kn =
let warn_unusable_identifier =
CWarnings.create ~name:"unusable-identifier" ~category:"parsing"
- (fun id -> strbrk "The Ltac name" ++ spc () ++ pr_id id ++ spc () ++
+ (fun id -> strbrk "The Ltac name" ++ spc () ++ Id.print id ++ spc () ++
strbrk "may be unusable because of a conflict with a notation.")
let register_ltac local tacl =
@@ -427,7 +427,7 @@ let register_ltac local tacl =
match tactic_body with
| Tacexpr.TacticDefinition ((loc,id), body) ->
let kn = Lib.make_kn id in
- let id_pp = pr_id id in
+ let id_pp = Id.print id in
let () = if is_defined_tac kn then
CErrors.user_err ?loc
(str "There is already an Ltac named " ++ id_pp ++ str".")
@@ -475,7 +475,7 @@ let register_ltac local tacl =
let iter (def, tac) = match def with
| NewTac id ->
Tacenv.register_ltac false local id tac;
- Flags.if_verbose Feedback.msg_info (Nameops.pr_id id ++ str " is defined")
+ Flags.if_verbose Feedback.msg_info (Id.print id ++ str " is defined")
| UpdateTac kn ->
Tacenv.redefine_ltac local kn tac;
let name = Nametab.shortest_qualid_of_tactic kn in
diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml
index 85d3944b1..9d8094205 100644
--- a/plugins/ltac/tacinterp.ml
+++ b/plugins/ltac/tacinterp.ml
@@ -92,7 +92,7 @@ type value = Val.t
(** Abstract application, to print ltac functions *)
type appl =
| UnnamedAppl (** For generic applications: nothing is printed *)
- | GlbAppl of (Names.kernel_name * Val.t list) list
+ | GlbAppl of (Names.KerName.t * Val.t list) list
(** For calls to global constants, some may alias other. *)
let push_appl appl args =
match appl with
@@ -257,7 +257,7 @@ let pr_closure env ist body =
let pr_sep () = fnl () in
let pr_iarg (id, arg) =
let arg = pr_argument_type arg in
- hov 0 (pr_id id ++ spc () ++ str ":" ++ spc () ++ arg)
+ hov 0 (Id.print id ++ spc () ++ str ":" ++ spc () ++ arg)
in
let pp_iargs = v 0 (prlist_with_sep pr_sep pr_iarg (Id.Map.bindings ist)) in
pp_body ++ fnl() ++ str "in environment " ++ fnl() ++ pp_iargs
@@ -314,7 +314,7 @@ let append_trace trace v =
let coerce_to_tactic loc id v =
let v = Value.normalize v in
let fail () = user_err ?loc
- (str "Variable " ++ pr_id id ++ str " should be bound to a tactic.")
+ (str "Variable " ++ Id.print id ++ str " should be bound to a tactic.")
in
let v = Value.normalize v in
if has_type v (topwit wit_tacvalue) then
@@ -369,7 +369,7 @@ let debugging_exception_step ist signal_anomaly e pp =
pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e)
let error_ltac_variable ?loc id env v s =
- user_err ?loc (str "Ltac variable " ++ pr_id id ++
+ user_err ?loc (str "Ltac variable " ++ Id.print id ++
strbrk " is bound to" ++ spc () ++ pr_value env v ++ spc () ++
strbrk "which cannot be coerced to " ++ str s ++ str".")
@@ -403,7 +403,7 @@ let interp_int ist locid =
try try_interp_ltac_var coerce_to_int ist None locid
with Not_found ->
user_err ?loc:(fst locid) ~hdr:"interp_int"
- (str "Unbound variable " ++ pr_id (snd locid) ++ str".")
+ (str "Unbound variable " ++ Id.print (snd locid) ++ str".")
let interp_int_or_var ist = function
| ArgVar locid -> interp_int ist locid
@@ -782,7 +782,7 @@ let interp_may_eval f ist env sigma = function
with
| Not_found ->
user_err ?loc ~hdr:"interp_may_eval"
- (str "Unbound context identifier" ++ pr_id s ++ str"."))
+ (str "Unbound context identifier" ++ Id.print s ++ str"."))
| ConstrTypeOf c ->
let (sigma,c_interp) = f ist env sigma c in
let (sigma, t) = Typing.type_of ~refresh:true env sigma c_interp in
@@ -858,7 +858,7 @@ let rec message_of_value v =
end
else if has_type v (topwit wit_var) then
let id = out_gen (topwit wit_var) v in
- Ftactic.enter begin fun gl -> Ftactic.return (pr_id id) end
+ Ftactic.enter begin fun gl -> Ftactic.return (Id.print id) end
else match Value.to_list v with
| Some l ->
Ftactic.List.map message_of_value l >>= fun l ->
@@ -873,7 +873,7 @@ let interp_message_token ist = function
| MsgIdent (loc,id) ->
let v = try Some (Id.Map.find id ist.lfun) with Not_found -> None in
match v with
- | None -> Ftactic.lift (Tacticals.New.tclZEROMSG (pr_id id ++ str" not found."))
+ | None -> Ftactic.lift (Tacticals.New.tclZEROMSG (Id.print id ++ str" not found."))
| Some v -> message_of_value v
let interp_message ist l =
@@ -1010,7 +1010,7 @@ let interp_destruction_arg ist gl arg =
| keep,ElimOnAnonHyp n as x -> x
| keep,ElimOnIdent (loc,id) ->
let error () = user_err ?loc
- (strbrk "Cannot coerce " ++ pr_id id ++
+ (strbrk "Cannot coerce " ++ Id.print id ++
strbrk " neither to a quantified hypothesis nor to a term.")
in
let try_cast_id id' =
@@ -1021,7 +1021,7 @@ let interp_destruction_arg ist gl arg =
try (sigma, (constr_of_id env id', NoBindings))
with Not_found ->
user_err ?loc ~hdr:"interp_destruction_arg" (
- pr_id id ++ strbrk " binds to " ++ pr_id id' ++ strbrk " which is neither a declared nor a quantified hypothesis.")
+ Id.print id ++ strbrk " binds to " ++ Id.print id' ++ strbrk " which is neither a declared nor a quantified hypothesis.")
end)
in
try
@@ -1088,7 +1088,7 @@ let read_pattern lfun ist env sigma = function
let cons_and_check_name id l =
if Id.List.mem id l then
user_err ~hdr:"read_match_goal_hyps" (
- str "Hypothesis pattern-matching variable " ++ pr_id id ++
+ str "Hypothesis pattern-matching variable " ++ Id.print id ++
str " used twice in the same pattern.")
else id::l
diff --git a/plugins/ltac/tactic_debug.ml b/plugins/ltac/tactic_debug.ml
index 8126421c7..b909c930d 100644
--- a/plugins/ltac/tactic_debug.ml
+++ b/plugins/ltac/tactic_debug.ml
@@ -12,8 +12,6 @@ open Names
open Pp
open Tacexpr
open Termops
-open Nameops
-
let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make ()
@@ -259,14 +257,14 @@ let db_pattern_rule debug num r =
(* Prints the hypothesis pattern identifier if it exists *)
let hyp_bound = function
| Anonymous -> str " (unbound)"
- | Name id -> str " (bound to " ++ pr_id id ++ str ")"
+ | Name id -> str " (bound to " ++ Id.print id ++ str ")"
(* Prints a matched hypothesis *)
let db_matched_hyp debug env sigma (id,_,c) ido =
let open Proofview.NonLogical in
is_debug debug >>= fun db ->
if db then
- msg_tac_debug (str "Hypothesis " ++ pr_id id ++ hyp_bound ido ++
+ msg_tac_debug (str "Hypothesis " ++ Id.print id ++ hyp_bound ido ++
str " has been matched: " ++ print_constr_env env sigma c)
else return ()
@@ -361,7 +359,7 @@ let explain_ltac_call_trace last trace loc =
| Tacexpr.LtacMLCall t ->
quote (Pptactic.pr_glob_tactic (Global.env()) t)
| Tacexpr.LtacVarCall (id,t) ->
- quote (Nameops.pr_id id) ++ strbrk " (bound to " ++
+ quote (Id.print id) ++ strbrk " (bound to " ++
Pptactic.pr_glob_tactic (Global.env()) t ++ str ")"
| Tacexpr.LtacAtomCall te ->
quote (Pptactic.pr_glob_tactic (Global.env())
@@ -372,7 +370,7 @@ let explain_ltac_call_trace last trace loc =
strbrk " (with " ++
prlist_with_sep pr_comma
(fun (id,c) ->
- pr_id id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
+ Id.print id ++ str ":=" ++ Printer.pr_lconstr_under_binders c)
(List.rev (Id.Map.bindings vars)) ++ str ")"
else mt())
in
diff --git a/plugins/ltac/tauto.ml b/plugins/ltac/tauto.ml
index 13492ed51..5eacb1a95 100644
--- a/plugins/ltac/tauto.ml
+++ b/plugins/ltac/tauto.ml
@@ -197,7 +197,7 @@ let flatten_contravariant_disj _ ist =
let make_unfold name =
let dir = DirPath.make (List.map Id.of_string ["Logic"; "Init"; "Coq"]) in
- let const = Constant.make2 (MPfile dir) (Label.make name) in
+ let const = Constant.make2 (ModPath.MPfile dir) (Label.make name) in
(Locus.AllOccurrences, ArgArg (EvalConstRef const, None))
let u_iff = make_unfold "iff"
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-27 03:25:04 +0000