aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/printers.mllib1
-rw-r--r--grammar/grammar.mllib28
-rw-r--r--interp/constrarg.mli10
-rw-r--r--interp/constrexpr_ops.ml14
-rw-r--r--interp/constrexpr_ops.mli3
-rw-r--r--interp/notation.ml12
-rw-r--r--interp/notation_ops.ml4
-rw-r--r--plugins/funind/g_indfun.ml43
-rw-r--r--pretyping/glob_ops.ml16
-rw-r--r--pretyping/glob_ops.mli1
-rw-r--r--pretyping/miscops.ml38
-rw-r--r--pretyping/miscops.mli10
-rw-r--r--pretyping/patternops.ml2
-rw-r--r--printing/miscprint.ml41
-rw-r--r--printing/miscprint.mli18
-rw-r--r--printing/pptactic.ml22
-rw-r--r--printing/printer.ml2
-rw-r--r--proofs/logic.ml2
-rw-r--r--proofs/proofs.mllib1
-rw-r--r--tactics/tacinterp.ml2
-rw-r--r--tactics/tactics.ml4
21 files changed, 125 insertions, 109 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib
index 0138f7034..82ef43a7d 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -157,6 +157,7 @@ Modintern
Constrextern
Proof_type
Goal
+Miscprint
Logic
Refiner
Clenv
diff --git a/grammar/grammar.mllib b/grammar/grammar.mllib
index b1c1c3c8e..3f5fc5e86 100644
--- a/grammar/grammar.mllib
+++ b/grammar/grammar.mllib
@@ -11,7 +11,6 @@ Pp_control
Flags
Pp
Loc
-Compat
Errors
Hashset
Hashcons
@@ -25,30 +24,33 @@ Predicate
Segmenttree
Unicodetable
Unicode
+Genarg
Evar
Names
+
Libnames
-Genarg
+
+Redops
+Miscops
+Locusops
+
Stdarg
Constrarg
+Constrexpr_ops
+
+Compat
Tok
Lexer
Pcoq
+G_prim
+G_tactic
+G_ltac
+G_constr
+
Q_util
Q_coqast
Egramml
Argextend
Tacextend
Vernacextend
-
-Nameops
-Redops
-Miscops
-Glob_ops
-Constrexpr_ops
-Locusops
-G_prim
-G_tactic
-G_ltac
-G_constr
diff --git a/interp/constrarg.mli b/interp/constrarg.mli
index 1654d2719..c49b61ce7 100644
--- a/interp/constrarg.mli
+++ b/interp/constrarg.mli
@@ -10,7 +10,6 @@
of Genarg in [constr]-related interfaces. *)
open Loc
-open Pp
open Names
open Term
open Libnames
@@ -20,9 +19,7 @@ open Genredexpr
open Pattern
open Constrexpr
open Tacexpr
-open Term
open Misctypes
-open Evd
open Genarg
(** FIXME: nothing to do there. *)
@@ -53,17 +50,18 @@ val wit_constr_may_eval :
(glob_constr_and_expr,evaluable_global_reference and_short_name or_var,glob_constr_pattern_and_expr) may_eval,
constr) genarg_type
-val wit_open_constr : (open_constr_expr, open_glob_constr, open_constr) genarg_type
+val wit_open_constr :
+ (open_constr_expr, open_glob_constr, Evd.open_constr) genarg_type
val wit_constr_with_bindings :
(constr_expr with_bindings,
glob_constr_and_expr with_bindings,
- constr with_bindings sigma) genarg_type
+ constr with_bindings Evd.sigma) genarg_type
val wit_bindings :
(constr_expr bindings,
glob_constr_and_expr bindings,
- constr bindings sigma) genarg_type
+ constr bindings Evd.sigma) genarg_type
val wit_red_expr :
((constr_expr,reference or_by_notation,constr_expr) red_expr_gen,
diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index c8a0e5638..85ad1cee7 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -10,7 +10,6 @@ open Pp
open Util
open Names
open Libnames
-open Glob_term
open Constrexpr
open Misctypes
open Decl_kinds
@@ -150,7 +149,7 @@ let rec constr_expr_eq e1 e2 =
Evar.equal ev1 ev2 &&
Option.equal (List.equal constr_expr_eq) c1 c2
| CSort(_,s1), CSort(_,s2) ->
- Glob_ops.glob_sort_eq s1 s2
+ Miscops.glob_sort_eq s1 s2
| CCast(_,a1,(CastConv b1|CastVM b1)), CCast(_,a2,(CastConv b2|CastVM b2)) ->
constr_expr_eq a1 a2 &&
constr_expr_eq b1 b2
@@ -336,14 +335,3 @@ let coerce_to_name = function
| a -> Errors.user_err_loc
(constr_loc a,"coerce_to_name",
str "This expression should be a name.")
-
-let rec raw_cases_pattern_expr_of_glob_constr looked_for = function
- | GVar (loc,id) -> RCPatAtom (loc,Some id)
- | GHole (loc,_,_) -> RCPatAtom (loc,None)
- | GRef (loc,g) ->
- looked_for g;
- RCPatCstr (loc, g,[],[])
- | GApp (loc,GRef (_,g),l) ->
- looked_for g;
- RCPatCstr (loc, g,List.map (raw_cases_pattern_expr_of_glob_constr looked_for) l,[])
- | _ -> raise Not_found
diff --git a/interp/constrexpr_ops.mli b/interp/constrexpr_ops.mli
index d857a5b60..687f5cb9e 100644
--- a/interp/constrexpr_ops.mli
+++ b/interp/constrexpr_ops.mli
@@ -82,6 +82,3 @@ val names_of_local_binders : local_binder list -> Name.t located list
val names_of_local_assums : local_binder list -> Name.t located list
(** Same as [names_of_local_binders], but does not take the [let] bindings into
account. *)
-
-val raw_cases_pattern_expr_of_glob_constr : (Globnames.global_reference -> unit)
- -> Glob_term.glob_constr -> raw_cases_pattern_expr
diff --git a/interp/notation.ml b/interp/notation.ml
index 867e23395..262cbab2f 100644
--- a/interp/notation.ml
+++ b/interp/notation.ml
@@ -449,8 +449,18 @@ let interp_prim_token_gen g loc p local_scopes =
let interp_prim_token =
interp_prim_token_gen (fun x -> x)
+(** [rcp_of_glob] : from [glob_constr] to [raw_cases_pattern_expr] *)
+
+let rec rcp_of_glob looked_for = function
+ | GVar (loc,id) -> RCPatAtom (loc,Some id)
+ | GHole (loc,_,_) -> RCPatAtom (loc,None)
+ | GRef (loc,g) -> looked_for g; RCPatCstr (loc, g,[],[])
+ | GApp (loc,GRef (_,g),l) ->
+ looked_for g; RCPatCstr (loc, g, List.map (rcp_of_glob looked_for) l,[])
+ | _ -> raise Not_found
+
let interp_prim_token_cases_pattern_expr loc looked_for p =
- interp_prim_token_gen (Constrexpr_ops.raw_cases_pattern_expr_of_glob_constr looked_for) loc p
+ interp_prim_token_gen (rcp_of_glob looked_for) loc p
let interp_notation loc ntn local_scopes =
let scopes = make_current_scopes local_scopes in
diff --git a/interp/notation_ops.ml b/interp/notation_ops.ml
index f6afbe48a..12b256c45 100644
--- a/interp/notation_ops.ml
+++ b/interp/notation_ops.ml
@@ -156,7 +156,7 @@ let compare_glob_constr f add t1 t2 = match t1,t2 with
when Name.equal na1 na2 && Constrexpr_ops.binding_kind_eq bk1 bk2 ->
on_true_do (f ty1 ty2 && f c1 c2) add na1
| GHole _, GHole _ -> true
- | GSort (_,s1), GSort (_,s2) -> glob_sort_eq s1 s2
+ | GSort (_,s1), GSort (_,s2) -> Miscops.glob_sort_eq s1 s2
| GLetIn (_,na1,b1,c1), GLetIn (_,na2,b2,c2) when Name.equal na1 na2 ->
on_true_do (f b1 b2 && f c1 c2) add na1
| (GCases _ | GRec _
@@ -721,7 +721,7 @@ let rec match_ inner u alp (tmetas,blmetas as metas) sigma a1 a2 =
| GCast(_,c1, CastCoerce), NCast(c2, CastCoerce) ->
match_in u alp metas sigma c1 c2
| GSort (_,GType _), NSort (GType None) when not u -> sigma
- | GSort (_,s1), NSort s2 when glob_sort_eq s1 s2 -> sigma
+ | GSort (_,s1), NSort s2 when Miscops.glob_sort_eq s1 s2 -> sigma
| GPatVar _, NHole _ -> (*Don't hide Metas, they bind in ltac*) raise No_match
| a, NHole _ -> sigma
diff --git a/plugins/funind/g_indfun.ml4 b/plugins/funind/g_indfun.ml4
index ca90b3759..cc9ae912d 100644
--- a/plugins/funind/g_indfun.ml4
+++ b/plugins/funind/g_indfun.ml4
@@ -78,7 +78,8 @@ END
let pr_intro_as_pat prc _ _ pat =
match pat with
- | Some pat -> spc () ++ str "as" ++ spc () ++ pr_intro_pattern pat
+ | Some pat ->
+ spc () ++ str "as" ++ spc () ++ Miscprint.pr_intro_pattern pat
| None -> mt ()
diff --git a/pretyping/glob_ops.ml b/pretyping/glob_ops.ml
index 9fc981a7d..f1e38d0f8 100644
--- a/pretyping/glob_ops.ml
+++ b/pretyping/glob_ops.ml
@@ -46,13 +46,6 @@ let case_style_eq s1 s2 = match s1, s2 with
| RegularStyle, RegularStyle -> true
| _ -> false
-let glob_sort_eq g1 g2 = match g1, g2 with
-| GProp, GProp -> true
-| GSet, GSet -> true
-| GType None, GType None -> true
-| GType (Some s1), GType (Some s2) -> String.equal s1 s2
-| _ -> false
-
let rec cases_pattern_eq p1 p2 = match p1, p2 with
| PatVar (_, na1), PatVar (_, na2) -> Name.equal na1 na2
| PatCstr (_, c1, pl1, na1), PatCstr (_, c2, pl2, na2) ->
@@ -67,13 +60,6 @@ let cast_type_eq eq t1 t2 = match t1, t2 with
| CastNative t1, CastNative t2 -> eq t1 t2
| _ -> false
-let eq_gr gr1 gr2 = match gr1, gr2 with
-| ConstRef con1, ConstRef con2 -> eq_constant con1 con2
-| IndRef kn1, IndRef kn2 -> eq_ind kn1 kn2
-| ConstructRef kn1, ConstructRef kn2 -> eq_constructor kn1 kn2
-| VarRef v1, VarRef v2 -> Id.equal v1 v2
-| _ -> false
-
let rec glob_constr_eq c1 c2 = match c1, c2 with
| GRef (_, gr1), GRef (_, gr2) -> eq_gr gr1 gr2
| GVar (_, id1), GVar (_, id2) -> Id.equal id1 id2
@@ -109,7 +95,7 @@ let rec glob_constr_eq c1 c2 = match c1, c2 with
Array.equal (fun l1 l2 -> List.equal glob_decl_eq l1 l2) decl1 decl2 &&
Array.equal glob_constr_eq c1 c2 &&
Array.equal glob_constr_eq t1 t2
-| GSort (_, s1), GSort (_, s2) -> glob_sort_eq s1 s2
+| GSort (_, s1), GSort (_, s2) -> Miscops.glob_sort_eq s1 s2
| GHole (_, kn1, gn1), GHole (_, kn2, gn2) ->
Option.equal (==) gn1 gn2 (** Only thing sensible *)
| GCast (_, c1, t1), GCast (_, c2, t2) ->
diff --git a/pretyping/glob_ops.mli b/pretyping/glob_ops.mli
index 5195b98c8..1785c87be 100644
--- a/pretyping/glob_ops.mli
+++ b/pretyping/glob_ops.mli
@@ -18,7 +18,6 @@ open Locus
open Glob_term
(** Equalities *)
-val glob_sort_eq : glob_sort -> glob_sort -> bool
val cases_pattern_eq : cases_pattern -> cases_pattern -> bool
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 2639e2e72..ab01065b1 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -7,8 +7,6 @@
(************************************************************************)
open Misctypes
-open Pp
-open Nameops
(** Mapping [cast_type] *)
@@ -25,33 +23,11 @@ let smartmap_cast_type f c =
| CastCoerce -> CastCoerce
| CastNative a -> let a' = f a in if a' == a then c else CastNative a'
-(** Printing of [intro_pattern] *)
+(** Equalities on [glob_sort] *)
-let rec pr_intro_pattern (_,pat) = match pat with
- | IntroOrAndPattern pll -> pr_or_and_intro_pattern pll
- | IntroInjection pl ->
- str "[=" ++ hv 0 (prlist_with_sep spc pr_intro_pattern pl) ++ str "]"
- | IntroWildcard -> str "_"
- | IntroRewrite true -> str "->"
- | IntroRewrite false -> str "<-"
- | IntroIdentifier id -> pr_id id
- | IntroFresh id -> str "?" ++ pr_id id
- | IntroForthcoming true -> str "*"
- | IntroForthcoming false -> str "**"
- | IntroAnonymous -> str "?"
-
-and pr_or_and_intro_pattern = function
- | [pl] ->
- str "(" ++ hv 0 (prlist_with_sep pr_comma pr_intro_pattern pl) ++ str ")"
- | pll ->
- str "[" ++
- hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
- ++ str "]"
-
-(** Printing of [move_location] *)
-
-let pr_move_location pr_id = function
- | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
- | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
- | MoveFirst -> str " at top"
- | MoveLast -> str " at bottom"
+let glob_sort_eq g1 g2 = match g1, g2 with
+| GProp, GProp -> true
+| GSet, GSet -> true
+| GType None, GType None -> true
+| GType (Some s1), GType (Some s2) -> CString.equal s1 s2
+| _ -> false
diff --git a/pretyping/miscops.mli b/pretyping/miscops.mli
index cf984113f..84541a3b2 100644
--- a/pretyping/miscops.mli
+++ b/pretyping/miscops.mli
@@ -13,12 +13,6 @@ open Misctypes
val map_cast_type : ('a -> 'b) -> 'a cast_type -> 'b cast_type
val smartmap_cast_type : ('a -> 'a) -> 'a cast_type -> 'a cast_type
-(** Printing of [intro_pattern] *)
+(** Equalities on [glob_sort] *)
-val pr_intro_pattern : intro_pattern_expr Loc.located -> Pp.std_ppcmds
-val pr_or_and_intro_pattern : or_and_intro_pattern_expr -> Pp.std_ppcmds
-
-(** Printing of [move_location] *)
-
-val pr_move_location :
- ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds
+val glob_sort_eq : glob_sort -> glob_sort -> bool
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index a2e8e4599..cc13d342a 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -45,7 +45,7 @@ let rec constr_pattern_eq p1 p2 = match p1, p2 with
Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
| PLetIn (v1, t1, b1), PLetIn (v2, t2, b2) ->
Name.equal v1 v2 && constr_pattern_eq t1 t2 && constr_pattern_eq b1 b2
-| PSort s1, PSort s2 -> glob_sort_eq s1 s2
+| PSort s1, PSort s2 -> Miscops.glob_sort_eq s1 s2
| PMeta m1, PMeta m2 -> Option.equal Id.equal m1 m2
| PIf (t1, l1, r1), PIf (t2, l2, r2) ->
constr_pattern_eq t1 t2 && constr_pattern_eq l1 l2 && constr_pattern_eq r1 r2
diff --git a/printing/miscprint.ml b/printing/miscprint.ml
new file mode 100644
index 000000000..3a0f7a8f7
--- /dev/null
+++ b/printing/miscprint.ml
@@ -0,0 +1,41 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Misctypes
+open Pp
+
+(** Printing of [intro_pattern] *)
+
+let rec pr_intro_pattern (_,pat) = match pat with
+ | IntroOrAndPattern pll -> pr_or_and_intro_pattern pll
+ | IntroInjection pl ->
+ str "[=" ++ hv 0 (prlist_with_sep spc pr_intro_pattern pl) ++ str "]"
+ | IntroWildcard -> str "_"
+ | IntroRewrite true -> str "->"
+ | IntroRewrite false -> str "<-"
+ | IntroIdentifier id -> Nameops.pr_id id
+ | IntroFresh id -> str "?" ++ Nameops.pr_id id
+ | IntroForthcoming true -> str "*"
+ | IntroForthcoming false -> str "**"
+ | IntroAnonymous -> str "?"
+
+and pr_or_and_intro_pattern = function
+ | [pl] ->
+ str "(" ++ hv 0 (prlist_with_sep pr_comma pr_intro_pattern pl) ++ str ")"
+ | pll ->
+ str "[" ++
+ hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc pr_intro_pattern) pll)
+ ++ str "]"
+
+(** Printing of [move_location] *)
+
+let pr_move_location pr_id = function
+ | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
+ | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
+ | MoveFirst -> str " at top"
+ | MoveLast -> str " at bottom"
diff --git a/printing/miscprint.mli b/printing/miscprint.mli
new file mode 100644
index 000000000..4e0be83f2
--- /dev/null
+++ b/printing/miscprint.mli
@@ -0,0 +1,18 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+open Misctypes
+
+(** Printing of [intro_pattern] *)
+
+val pr_intro_pattern : intro_pattern_expr Loc.located -> Pp.std_ppcmds
+
+(** Printing of [move_location] *)
+
+val pr_move_location :
+ ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index ae3b41e23..adb2ba0d0 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -18,7 +18,6 @@ open Constrarg
open Libnames
open Ppextend
open Misctypes
-open Miscops
open Locus
open Decl_kinds
open Genredexpr
@@ -342,8 +341,8 @@ let pr_bindings prlc prc = pr_bindings_gen false prlc prc
let pr_with_bindings prlc prc (c,bl) =
hov 1 (prc c ++ pr_bindings prlc prc bl)
-let pr_as_ipat pat = str "as " ++ pr_intro_pattern pat
-let pr_eqn_ipat pat = str "eqn:" ++ pr_intro_pattern pat
+let pr_as_ipat pat = str "as " ++ Miscprint.pr_intro_pattern pat
+let pr_eqn_ipat pat = str "eqn:" ++ Miscprint.pr_intro_pattern pat
let pr_with_induction_names = function
| None, None -> mt ()
@@ -353,7 +352,7 @@ let pr_with_induction_names = function
spc () ++ hov 1 (pr_as_ipat ipat ++ spc () ++ pr_eqn_ipat eqpat)
let pr_as_intro_pattern ipat =
- spc () ++ hov 1 (str "as" ++ spc () ++ pr_intro_pattern ipat)
+ spc () ++ hov 1 (str "as" ++ spc () ++ Miscprint.pr_intro_pattern ipat)
let pr_with_inversion_names = function
| None -> mt ()
@@ -645,13 +644,15 @@ and pr_atom1 = function
(* Basic tactics *)
| TacIntroPattern [] as t -> pr_atom0 t
| TacIntroPattern (_::_ as p) ->
- hov 1 (str "intros" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p)
+ hov 1 (str "intros" ++ spc () ++
+ prlist_with_sep spc Miscprint.pr_intro_pattern p)
| TacIntrosUntil h ->
hv 1 (str "intros until" ++ pr_arg pr_quantified_hypothesis h)
| TacIntroMove (None,MoveLast) as t -> pr_atom0 t
| TacIntroMove (Some id,MoveLast) -> str "intro " ++ pr_id id
| TacIntroMove (ido,hto) ->
- hov 1 (str"intro" ++ pr_opt pr_id ido ++ Miscops.pr_move_location pr_ident hto)
+ hov 1 (str"intro" ++ pr_opt pr_id ido ++
+ Miscprint.pr_move_location pr_ident hto)
| TacAssumption as t -> pr_atom0 t
| TacExact c -> hov 1 (str "exact" ++ pr_constrarg c)
| TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c)
@@ -764,7 +765,7 @@ and pr_atom1 = function
assert b;
hov 1
(str "move" ++ brk (1,1) ++ pr_ident id1 ++
- Miscops.pr_move_location pr_ident id2)
+ Miscprint.pr_move_location pr_ident id2)
| TacRename l ->
hov 1
(str "rename" ++ brk (1,1) ++
@@ -1033,8 +1034,11 @@ let () =
let pr_string s = str "\"" ++ str s ++ str "\"" in
Genprint.register_print0 Constrarg.wit_ref
pr_reference (pr_or_var (pr_located pr_global)) pr_global;
- Genprint.register_print0 Constrarg.wit_intro_pattern
- pr_intro_pattern pr_intro_pattern pr_intro_pattern;
+ Genprint.register_print0
+ Constrarg.wit_intro_pattern
+ Miscprint.pr_intro_pattern
+ Miscprint.pr_intro_pattern
+ Miscprint.pr_intro_pattern;
Genprint.register_print0 Constrarg.wit_sort
pr_glob_sort pr_glob_sort pr_sort;
Genprint.register_print0 Stdarg.wit_int int int int;
diff --git a/printing/printer.ml b/printing/printer.ml
index 85b3c1836..9143d1c5b 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -647,7 +647,7 @@ let pr_prim_rule = function
| Move (withdep,id1,id2) ->
(str (if withdep then "dependent " else "") ++
- str"move " ++ pr_id id1 ++ Miscops.pr_move_location pr_id id2)
+ str"move " ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2)
| Order ord ->
(str"order " ++ pr_sequence pr_id ord)
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 68be51d9c..1116410dc 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -279,7 +279,7 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
(first, d::middle)
else
errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id idfrom ++
- Miscops.pr_move_location pr_id hto ++
+ Miscprint.pr_move_location pr_id hto ++
str (if toleft then ": it occurs in " else ": it depends on ")
++ pr_id hyp ++ str ".")
else
diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib
index 96b9a89a3..ab5cf52d4 100644
--- a/proofs/proofs.mllib
+++ b/proofs/proofs.mllib
@@ -1,3 +1,4 @@
+Miscprint
Goal
Evar_refiner
Proof_using
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index c802ae984..cd265843d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -696,7 +696,7 @@ let rec message_of_value gl v =
else if has_type v (topwit wit_unit) then str "()"
else if has_type v (topwit wit_int) then int (out_gen (topwit wit_int) v)
else if has_type v (topwit wit_intro_pattern) then
- pr_intro_pattern (out_gen (topwit wit_intro_pattern) v)
+ Miscprint.pr_intro_pattern (out_gen (topwit wit_intro_pattern) v)
else if has_type v (topwit wit_constr_context) then
pr_constr_env (pf_env gl) (out_gen (topwit wit_constr_context) v)
else match Value.to_list v with
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index fe26bbb2d..d1b096048 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -2085,7 +2085,7 @@ let check_unused_names names =
if not (List.is_empty names) && Flags.is_verbose () then
msg_warning
(str"Unused introduction " ++ str (String.plural (List.length names) "pattern")
- ++ str": " ++ prlist_with_sep spc pr_intro_pattern names)
+ ++ str": " ++ prlist_with_sep spc Miscprint.pr_intro_pattern names)
let rec consume_pattern avoid id isdep gl = function
| [] -> ((dloc, IntroIdentifier (fresh_id avoid id gl)), [])
@@ -3380,7 +3380,7 @@ let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
let new_induct_gen_l isrec with_evars elim (eqname,names) lc =
if not (Option.is_empty eqname) then
errorlabstrm "" (str "Do not know what to do with " ++
- pr_intro_pattern (Option.get eqname));
+ Miscprint.pr_intro_pattern (Option.get eqname));
let newlc = ref [] in
let letids = ref [] in
let rec atomize_list l =
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 09:24:05 +0000