aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cbv.ml11
-rw-r--r--pretyping/coercionops.ml238
-rw-r--r--pretyping/coercionops.mli40
-rw-r--r--pretyping/detyping.ml10
-rw-r--r--pretyping/dune2
-rw-r--r--pretyping/evarconv.ml105
-rw-r--r--pretyping/inductiveops.ml65
-rw-r--r--pretyping/inductiveops.mli6
-rw-r--r--pretyping/nativenorm.ml23
-rw-r--r--pretyping/pretyping.ml7
-rw-r--r--pretyping/reductionops.ml16
-rw-r--r--pretyping/reductionops.mli2
-rw-r--r--pretyping/tacred.ml4
-rw-r--r--pretyping/unification.ml15
14 files changed, 228 insertions, 316 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 7930c3d634..02fb347d08 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -201,10 +201,7 @@ let cofixp_reducible flgs _ stk =
else
false
-let get_debug_cbv = Goptions.declare_bool_option_and_ref
- ~depr:false
- ~value:false
- ~key:["Debug";"Cbv"]
+let debug_cbv = CDebug.create ~name:"Cbv" ()
(* Reduction of primitives *)
@@ -525,7 +522,7 @@ and norm_head_ref k info env stack normt t =
if red_set_ref info.reds normt then
match cbv_value_cache info normt with
| Declarations.Def body ->
- if get_debug_cbv () then Feedback.msg_debug Pp.(str "Unfolding " ++ debug_pr_key normt);
+ debug_cbv (fun () -> Pp.(str "Unfolding " ++ debug_pr_key normt));
strip_appl (shift_value k body) stack
| Declarations.Primitive op ->
let c = match normt with
@@ -534,11 +531,11 @@ and norm_head_ref k info env stack normt t =
in
(PRIMITIVE(op,c,[||]),stack)
| Declarations.OpaqueDef _ | Declarations.Undef _ ->
- if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt);
+ debug_cbv (fun () -> Pp.(str "Not unfolding " ++ debug_pr_key normt));
(VAL(0,make_constr_ref k normt t),stack)
else
begin
- if get_debug_cbv () then Feedback.msg_debug Pp.(str "Not unfolding " ++ debug_pr_key normt);
+ debug_cbv (fun () -> Pp.(str "Not unfolding " ++ debug_pr_key normt));
(VAL(0,make_constr_ref k normt t),stack)
end
diff --git a/pretyping/coercionops.ml b/pretyping/coercionops.ml
index 8ddc576d83..274dbfd7ed 100644
--- a/pretyping/coercionops.ml
+++ b/pretyping/coercionops.ml
@@ -34,6 +34,31 @@ type cl_info_typ = {
cl_param : int
}
+let cl_typ_ord t1 t2 = match t1, t2 with
+ | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
+ | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2
+ | CL_PROJ c1, CL_PROJ c2 -> Projection.Repr.CanOrd.compare c1 c2
+ | CL_IND i1, CL_IND i2 -> Ind.CanOrd.compare i1 i2
+ | _ -> pervasives_compare t1 t2 (** OK *)
+
+let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0
+
+module ClTyp = struct
+ type t = cl_typ
+ let compare = cl_typ_ord
+end
+
+module ClPairOrd =
+struct
+ type t = cl_typ * cl_typ
+ let compare (i1, j1) (i2, j2) =
+ let c = cl_typ_ord i1 i2 in
+ if Int.equal c 0 then cl_typ_ord j1 j2 else c
+end
+
+module ClTypMap = Map.Make(ClTyp)
+module ClPairMap = Map.Make(ClPairOrd)
+
type coe_typ = GlobRef.t
module CoeTypMap = GlobRef.Map_env
@@ -43,6 +68,8 @@ type coe_info_typ = {
coe_local : bool;
coe_is_identity : bool;
coe_is_projection : Projection.Repr.t option;
+ coe_source : cl_typ;
+ coe_target : cl_typ;
coe_param : int;
}
@@ -53,88 +80,26 @@ let coe_info_typ_equal c1 c2 =
c1.coe_is_projection == c2.coe_is_projection &&
Int.equal c1.coe_param c2.coe_param
-let cl_typ_ord t1 t2 = match t1, t2 with
- | CL_SECVAR v1, CL_SECVAR v2 -> Id.compare v1 v2
- | CL_CONST c1, CL_CONST c2 -> Constant.CanOrd.compare c1 c2
- | CL_PROJ c1, CL_PROJ c2 -> Projection.Repr.CanOrd.compare c1 c2
- | CL_IND i1, CL_IND i2 -> Ind.CanOrd.compare i1 i2
- | _ -> pervasives_compare t1 t2 (** OK *)
-
-module ClTyp = struct
- type t = cl_typ
- let compare = cl_typ_ord
-end
-
-module ClTypMap = Map.Make(ClTyp)
-
-let cl_typ_eq t1 t2 = Int.equal (cl_typ_ord t1 t2) 0
-
type inheritance_path = coe_info_typ list
-(* table des classes, des coercions et graphe d'heritage *)
-
-module Bijint :
-sig
- module Index :
- sig
- type t
- val compare : t -> t -> int
- val equal : t -> t -> bool
- val print : t -> Pp.t
- end
- type 'a t
- val empty : 'a t
- val mem : cl_typ -> 'a t -> bool
- val map : Index.t -> 'a t -> cl_typ * 'a
- val revmap : cl_typ -> 'a t -> Index.t * 'a
- val add : cl_typ -> 'a -> 'a t -> 'a t
- val dom : 'a t -> cl_typ list
-end
-=
-struct
-
- module Index = struct include Int let print = Pp.int end
-
- type 'a t = { v : (cl_typ * 'a) Int.Map.t; s : int; inv : int ClTypMap.t }
- let empty = { v = Int.Map.empty; s = 0; inv = ClTypMap.empty }
- let mem y b = ClTypMap.mem y b.inv
- let map x b = Int.Map.find x b.v
- let revmap y b = let n = ClTypMap.find y b.inv in (n, snd (Int.Map.find n b.v))
- let add x y b =
- { v = Int.Map.add b.s (x,y) b.v; s = b.s+1; inv = ClTypMap.add x b.s b.inv }
- let dom b = List.rev (ClTypMap.fold (fun x _ acc -> x::acc) b.inv [])
-end
-
-type cl_index = Bijint.Index.t
-
let init_class_tab =
- let open Bijint in
+ let open ClTypMap in
add CL_FUN { cl_param = 0 } (add CL_SORT { cl_param = 0 } empty)
let class_tab =
- Summary.ref ~name:"class_tab" (init_class_tab : cl_info_typ Bijint.t)
+ Summary.ref ~name:"class_tab" (init_class_tab : cl_info_typ ClTypMap.t)
let coercion_tab =
Summary.ref ~name:"coercion_tab" (CoeTypMap.empty : coe_info_typ CoeTypMap.t)
-module ClPairOrd =
-struct
- type t = cl_index * cl_index
- let compare (i1, j1) (i2, j2) =
- let c = Bijint.Index.compare i1 i2 in
- if Int.equal c 0 then Bijint.Index.compare j1 j2 else c
-end
-
-module ClPairMap = Map.Make(ClPairOrd)
-
let inheritance_graph =
Summary.ref ~name:"inheritance_graph" (ClPairMap.empty : inheritance_path ClPairMap.t)
(* ajout de nouveaux "objets" *)
let add_new_class cl s =
- if not (Bijint.mem cl !class_tab) then
- class_tab := Bijint.add cl s !class_tab
+ if not (ClTypMap.mem cl !class_tab) then
+ class_tab := ClTypMap.add cl s !class_tab
let add_new_coercion coe s =
coercion_tab := CoeTypMap.add coe s !coercion_tab
@@ -144,19 +109,9 @@ let add_new_path x y =
(* class_info : cl_typ -> int * cl_info_typ *)
-let class_info cl = Bijint.revmap cl !class_tab
-
-let class_exists cl = Bijint.mem cl !class_tab
-
-(* class_info_from_index : int -> cl_typ * cl_info_typ *)
+let class_info cl = ClTypMap.find cl !class_tab
-let class_info_from_index i = Bijint.map i !class_tab
-
-let cl_fun_index = fst(class_info CL_FUN)
-
-let cl_sort_index = fst(class_info CL_SORT)
-
-(* coercion_info : coe_typ -> coe_info_typ *)
+let class_exists cl = ClTypMap.mem cl !class_tab
let coercion_info coe = CoeTypMap.find coe !coercion_tab
@@ -202,20 +157,18 @@ let subst_coe_typ subst t = subst_global_reference subst t
(* class_of : Term.constr -> int *)
let class_of env sigma t =
- let (t, n1, i, u, args) =
+ let (t, n1, cl, u, args) =
try
let (cl, u, args) = find_class_type env sigma t in
- let (i, { cl_param = n1 } ) = class_info cl in
- (t, n1, i, u, args)
+ let { cl_param = n1 } = class_info cl in
+ (t, n1, cl, u, args)
with Not_found ->
let t = Tacred.hnf_constr env sigma t in
let (cl, u, args) = find_class_type env sigma t in
- let (i, { cl_param = n1 } ) = class_info cl in
- (t, n1, i, u, args)
+ let { cl_param = n1 } = class_info cl in
+ (t, n1, cl, u, args)
in
- if Int.equal (List.length args) n1 then t, i else raise Not_found
-
-let inductive_class_of ind = fst (class_info (CL_IND ind))
+ if Int.equal (List.length args) n1 then t, cl else raise Not_found
let class_args_of env sigma c = pi3 (find_class_type env sigma c)
@@ -240,26 +193,26 @@ let lookup_path_between_class (s,t) =
ClPairMap.find (s,t) !inheritance_graph
let lookup_path_to_fun_from_class s =
- lookup_path_between_class (s,cl_fun_index)
+ lookup_path_between_class (s, CL_FUN)
let lookup_path_to_sort_from_class s =
- lookup_path_between_class (s,cl_sort_index)
+ lookup_path_between_class (s, CL_SORT)
(* advanced path lookup *)
let apply_on_class_of env sigma t cont =
try
let (cl,u,args) = find_class_type env sigma t in
- let (i, { cl_param = n1 } ) = class_info cl in
+ let { cl_param = n1 } = class_info cl in
if not (Int.equal (List.length args) n1) then raise Not_found;
- t, cont i
+ t, cont cl
with Not_found ->
(* Is it worth to be more incremental on the delta steps? *)
let t = Tacred.hnf_constr env sigma t in
let (cl, u, args) = find_class_type env sigma t in
- let (i, { cl_param = n1 } ) = class_info cl in
+ let { cl_param = n1 } = class_info cl in
if not (Int.equal (List.length args) n1) then raise Not_found;
- t, cont i
+ t, cont cl
let lookup_path_between env sigma (s,t) =
let (s,(t,p)) =
@@ -289,25 +242,25 @@ let get_coercion_constructor env coe =
| _ -> raise Not_found
let lookup_pattern_path_between env (s,t) =
- let i = inductive_class_of s in
- let j = inductive_class_of t in
- List.map (get_coercion_constructor env) (ClPairMap.find (i,j) !inheritance_graph)
+ List.map (get_coercion_constructor env)
+ (ClPairMap.find (CL_IND s, CL_IND t) !inheritance_graph)
(* rajouter une coercion dans le graphe *)
-let path_printer : ((cl_index * cl_index) * inheritance_path -> Pp.t) ref =
+let path_printer : ((cl_typ * cl_typ) * inheritance_path -> Pp.t) ref =
ref (fun _ -> str "<a class path>")
let install_path_printer f = path_printer := f
let print_path x = !path_printer x
-let path_comparator : (Environ.env -> Evd.evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) ref =
+let path_comparator :
+ (Environ.env -> Evd.evar_map -> cl_typ -> inheritance_path -> inheritance_path -> bool) ref =
ref (fun _ _ _ _ _ -> false)
let install_path_comparator f = path_comparator := f
-let compare_path p q = !path_comparator p q
+let compare_path env sigma cl p q = !path_comparator env sigma cl p q
let warn_ambiguous_path =
CWarnings.create ~name:"ambiguous-paths" ~category:"typechecker"
@@ -318,29 +271,29 @@ let warn_ambiguous_path =
else
str" is ambiguous with existing " ++ print_path (c, q) ++ str".") l)
-(* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
+(* add_coercion_in_graph : coe_index * cl_typ * cl_typ -> unit
coercion,source,target *)
-let different_class_params env i =
- let ci = class_info_from_index i in
- if (snd ci).cl_param > 0 then true
- else
- match fst ci with
- | CL_IND i -> Environ.is_polymorphic env (GlobRef.IndRef i)
- | CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c)
- | _ -> false
+let different_class_params env ci =
+ if (class_info ci).cl_param > 0 then true
+ else
+ match ci with
+ | CL_IND i -> Environ.is_polymorphic env (GlobRef.IndRef i)
+ | CL_CONST c -> Environ.is_polymorphic env (GlobRef.ConstRef c)
+ | _ -> false
-let add_coercion_in_graph env sigma (ic,source,target) =
+let add_coercion_in_graph env sigma ic =
let old_inheritance_graph = !inheritance_graph in
- let ambig_paths =
- (ref [] : ((cl_index * cl_index) * inheritance_path * inheritance_path) list ref) in
+ let ambig_paths :
+ ((cl_typ * cl_typ) * inheritance_path * inheritance_path) list ref =
+ ref [] in
let try_add_new_path (i,j as ij) p =
(* If p is a cycle, we check whether p is definitionally an identity
function or not. If it is not, we report p as an ambiguous inheritance
path. *)
- if Bijint.Index.equal i j && not (compare_path env sigma i p []) then
+ if cl_typ_eq i j && not (compare_path env sigma i p []) then
ambig_paths := (ij,p,[])::!ambig_paths;
- if not (Bijint.Index.equal i j) || different_class_params env i then
+ if not (cl_typ_eq i j) || different_class_params env i then
match lookup_path_between_class ij with
| q ->
(* p has the same source and target classes as an existing path q. We
@@ -361,45 +314,36 @@ let add_coercion_in_graph env sigma (ic,source,target) =
let try_add_new_path1 ij p =
let _ = try_add_new_path ij p in ()
in
- if try_add_new_path (source,target) [ic] then begin
+ if try_add_new_path (ic.coe_source, ic.coe_target) [ic] then begin
ClPairMap.iter
(fun (s,t) p ->
- if not (Bijint.Index.equal s t) then begin
- if Bijint.Index.equal t source then begin
- try_add_new_path1 (s,target) (p@[ic]);
+ if not (cl_typ_eq s t) then begin
+ if cl_typ_eq t ic.coe_source then begin
+ try_add_new_path1 (s, ic.coe_target) (p@[ic]);
ClPairMap.iter
(fun (u,v) q ->
- if not (Bijint.Index.equal u v) && Bijint.Index.equal u target then
+ if not (cl_typ_eq u v) && cl_typ_eq u ic.coe_target then
try_add_new_path1 (s,v) (p@[ic]@q))
old_inheritance_graph
end;
- if Bijint.Index.equal s target then try_add_new_path1 (source,t) (ic::p)
+ if cl_typ_eq s ic.coe_target then
+ try_add_new_path1 (ic.coe_source, t) (ic::p)
end)
old_inheritance_graph
end;
match !ambig_paths with [] -> () | _ -> warn_ambiguous_path !ambig_paths
-type coercion = {
- coercion_type : coe_typ;
- coercion_local : bool;
- coercion_is_id : bool;
- coercion_is_proj : Projection.Repr.t option;
- coercion_source : cl_typ;
- coercion_target : cl_typ;
- coercion_params : int;
-}
-
let subst_coercion subst c =
let env = Global.env () in
- let coe = subst_coe_typ subst c.coercion_type in
- let cls = subst_cl_typ env subst c.coercion_source in
- let clt = subst_cl_typ env subst c.coercion_target in
- let clp = Option.Smart.map (subst_proj_repr subst) c.coercion_is_proj in
- if c.coercion_type == coe && c.coercion_source == cls &&
- c.coercion_target == clt && c.coercion_is_proj == clp
+ let coe = subst_coe_typ subst c.coe_value in
+ let cls = subst_cl_typ env subst c.coe_source in
+ let clt = subst_cl_typ env subst c.coe_target in
+ let clp = Option.Smart.map (subst_proj_repr subst) c.coe_is_projection in
+ if c.coe_value == coe && c.coe_source == cls && c.coe_target == clt &&
+ c.coe_is_projection == clp
then c
- else { c with coercion_type = coe; coercion_source = cls;
- coercion_target = clt; coercion_is_proj = clp; }
+ else { c with coe_value = coe; coe_source = cls; coe_target = clt;
+ coe_is_projection = clp; }
(* Computation of the class arity *)
@@ -424,24 +368,14 @@ let add_class env sigma cl =
add_new_class cl { cl_param = class_params env sigma cl }
let declare_coercion env sigma c =
- let () = add_class env sigma c.coercion_source in
- let () = add_class env sigma c.coercion_target in
- let is, _ = class_info c.coercion_source in
- let it, _ = class_info c.coercion_target in
- let xf =
- { coe_value = c.coercion_type;
- coe_local = c.coercion_local;
- coe_is_identity = c.coercion_is_id;
- coe_is_projection = c.coercion_is_proj;
- coe_param = c.coercion_params;
- } in
- let () = add_new_coercion c.coercion_type xf in
- add_coercion_in_graph env sigma (xf,is,it)
+ let () = add_class env sigma c.coe_source in
+ let () = add_class env sigma c.coe_target in
+ let () = add_new_coercion c.coe_value c in
+ add_coercion_in_graph env sigma c
(* For printing purpose *)
-let pr_cl_index = Bijint.Index.print
-
-let classes () = Bijint.dom !class_tab
+let classes () =
+ List.rev (ClTypMap.fold (fun x _ acc -> x :: acc) !class_tab [])
let coercions () =
List.rev (CoeTypMap.fold (fun _ y acc -> y::acc) !coercion_tab [])
diff --git a/pretyping/coercionops.mli b/pretyping/coercionops.mli
index 31600dd17f..fb5621dd3a 100644
--- a/pretyping/coercionops.mli
+++ b/pretyping/coercionops.mli
@@ -44,12 +44,11 @@ type coe_info_typ = {
coe_local : bool;
coe_is_identity : bool;
coe_is_projection : Projection.Repr.t option;
+ coe_source : cl_typ;
+ coe_target : cl_typ;
coe_param : int;
}
-(** [cl_index] is the type of class keys *)
-type cl_index
-
(** This is the type of paths from a class to another *)
type inheritance_path = coe_info_typ list
@@ -57,46 +56,32 @@ type inheritance_path = coe_info_typ list
val class_exists : cl_typ -> bool
-val class_info : cl_typ -> (cl_index * cl_info_typ)
(** @raise Not_found if this type is not a class *)
-
-val class_info_from_index : cl_index -> cl_typ * cl_info_typ
+val class_info : cl_typ -> cl_info_typ
(** [find_class_type env sigma c] returns the head reference of [c],
its universe instance and its arguments *)
val find_class_type : env -> evar_map -> types -> cl_typ * EInstance.t * constr list
(** raises [Not_found] if not convertible to a class *)
-val class_of : env -> evar_map -> types -> types * cl_index
-
-(** raises [Not_found] if not mapped to a class *)
-val inductive_class_of : inductive -> cl_index
+val class_of : env -> evar_map -> types -> types * cl_typ
val class_args_of : env -> evar_map -> types -> constr list
-(** {6 [declare_coercion] adds a coercion in the graph of coercion paths } *)
-type coercion = {
- coercion_type : coe_typ;
- coercion_local : bool;
- coercion_is_id : bool;
- coercion_is_proj : Projection.Repr.t option;
- coercion_source : cl_typ;
- coercion_target : cl_typ;
- coercion_params : int;
-}
-
-val subst_coercion : substitution -> coercion -> coercion
+val subst_coercion : substitution -> coe_info_typ -> coe_info_typ
-val declare_coercion : env -> evar_map -> coercion -> unit
+val declare_coercion : env -> evar_map -> coe_info_typ -> unit
(** {6 Access to coercions infos } *)
val coercion_exists : coe_typ -> bool
+val coercion_info : coe_typ -> coe_info_typ
+
(** {6 Lookup functions for coercion paths } *)
(** @raise Not_found in the following functions when no path exists *)
-val lookup_path_between_class : cl_index * cl_index -> inheritance_path
+val lookup_path_between_class : cl_typ * cl_typ -> inheritance_path
val lookup_path_between : env -> evar_map -> types * types ->
types * types * inheritance_path
val lookup_path_to_fun_from : env -> evar_map -> types ->
@@ -109,16 +94,15 @@ val lookup_pattern_path_between :
(**/**)
(* Crade *)
val install_path_printer :
- ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
+ ((cl_typ * cl_typ) * inheritance_path -> Pp.t) -> unit
val install_path_comparator :
- (env -> evar_map -> cl_index -> inheritance_path -> inheritance_path -> bool) -> unit
+ (env -> evar_map -> cl_typ -> inheritance_path -> inheritance_path -> bool) -> unit
(**/**)
(** {6 This is for printing purpose } *)
val string_of_class : cl_typ -> string
val pr_class : cl_typ -> Pp.t
-val pr_cl_index : cl_index -> Pp.t
-val inheritance_graph : unit -> ((cl_index * cl_index) * inheritance_path) list
+val inheritance_graph : unit -> ((cl_typ * cl_typ) * inheritance_path) list
val classes : unit -> cl_typ list
val coercions : unit -> coe_info_typ list
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index c5f23482c7..48f34e7c6b 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -930,10 +930,12 @@ and detype_binder d flags bk avoid env sigma decl c =
let c = detype d { flags with flg_isgoal = false } avoid env sigma (Option.get body) in
(* Heuristic: we display the type if in Prop *)
let s =
- (* It can fail if ty is an evar, or if run inside ocamldebug or the
- OCaml toplevel since their printers don't have access to the proper sigma/env *)
- try Retyping.get_sort_family_of (snd env) sigma ty
- with Retyping.RetypeError _ -> InType
+ if !Flags.in_debugger then InType
+ else
+ (* It can fail if ty is an evar, or if run inside ocamldebug or the
+ OCaml toplevel since their printers don't have access to the proper sigma/env *)
+ try Retyping.get_sort_family_of (snd env) sigma ty
+ with Retyping.RetypeError _ -> InType
in
let t = if s != InProp && not !Flags.raw_print then None else Some (detype d { flags with flg_isgoal = false } avoid env sigma ty) in
GLetIn (na', c, t, r)
diff --git a/pretyping/dune b/pretyping/dune
index 14bce92de1..d9b5609bd4 100644
--- a/pretyping/dune
+++ b/pretyping/dune
@@ -1,6 +1,6 @@
(library
(name pretyping)
(synopsis "Coq's Type Inference Component (Pretyper)")
- (public_name coq.pretyping)
+ (public_name coq-core.pretyping)
(wrapped false)
(libraries engine))
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 990e84e5a7..e1d6fff3e4 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -47,17 +47,9 @@ let default_flags env =
let ts = default_transparent_state env in
default_flags_of ts
-let debug_unification =
- Goptions.declare_bool_option_and_ref
- ~depr:false
- ~key:["Debug";"Unification"]
- ~value:false
-
-let debug_ho_unification =
- Goptions.declare_bool_option_and_ref
- ~depr:false
- ~key:["Debug";"HO";"Unification"]
- ~value:false
+let debug_unification = CDebug.create ~name:"unification" ()
+
+let debug_ho_unification = CDebug.create ~name:"ho-unification" ()
(*******************************************)
(* Functions to deal with impossible cases *)
@@ -808,9 +800,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) flags env evd pbty
in
let app_empty = match sk1, sk2 with [], [] -> true | _ -> false in
(* Evar must be undefined since we have flushed evars *)
- let () = if debug_unification () then
- let open Pp in
- Feedback.msg_debug (v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ())) in
+ let () = debug_unification (fun () -> Pp.(v 0 (pr_state env evd appr1 ++ cut () ++ pr_state env evd appr2 ++ cut ()))) in
match (flex_kind_of_term flags env evd term1 sk1,
flex_kind_of_term flags env evd term2 sk2) with
| Flexible (sp1,al1), Flexible (sp2,al2) ->
@@ -1288,17 +1278,17 @@ let apply_on_subterm env evd fixed f test c t =
(fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
applyrec acc t
else
- (if debug_ho_unification () then
- Feedback.msg_debug Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t);
+ (debug_ho_unification (fun () ->
+ Pp.(str"Testing " ++ prc env !evdref c ++ str" against " ++ prc env !evdref t));
let b, evd =
try test env !evdref k c t
with e when CErrors.noncritical e -> assert false in
- if b then (if debug_ho_unification () then Feedback.msg_debug (Pp.str "succeeded");
+ if b then (debug_ho_unification (fun () -> Pp.str "succeeded");
let evd', fixed, t' = f !evdref !fixedref k t in
fixedref := fixed;
evdref := evd'; t')
else (
- if debug_ho_unification () then Feedback.msg_debug (Pp.str "failed");
+ debug_ho_unification (fun () -> Pp.str "failed");
map_constr_with_binders_left_to_right env !evdref
(fun d (env,(k,c)) -> (push_rel d env, (k+1,lift 1 c)))
applyrec acc t))
@@ -1404,9 +1394,9 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
let env_evar = evar_filtered_env env_rhs evi in
let sign = named_context_val env_evar in
let ctxt = evar_filtered_context evi in
- if debug_ho_unification () then
- (Feedback.msg_debug Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs);
- Feedback.msg_debug Pp.(str"env evars: " ++ Termops.Internal.print_env env_evar));
+ debug_ho_unification (fun () ->
+ Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs ++ fnl () ++
+ str"env evars: " ++ Termops.Internal.print_env env_evar));
let args = List.map (nf_evar evd) args in
let argsubst = List.map2 (fun decl c -> (NamedDecl.get_id decl, c)) ctxt args in
let instance = evar_identity_subst evi in
@@ -1439,17 +1429,17 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
let rec set_holes env_rhs evd fixed rhs = function
| (id,idty,c,cty,evsref,filter,occs)::subst ->
let c = nf_evar evd c in
- if debug_ho_unification () then
- Feedback.msg_debug Pp.(str"set holes for: " ++
+ debug_ho_unification (fun () ->
+ Pp.(str"set holes for: " ++
prc env_rhs evd (mkVar id.binder_name) ++ spc () ++
prc env_rhs evd c ++ str" in " ++
- prc env_rhs evd rhs);
+ prc env_rhs evd rhs));
let occ = ref 1 in
let set_var evd fixed k inst =
let oc = !occ in
- if debug_ho_unification () then
- (Feedback.msg_debug Pp.(str"Found one occurrence");
- Feedback.msg_debug Pp.(str"cty: " ++ prc env_rhs evd c));
+ debug_ho_unification (fun () ->
+ Pp.(str"Found one occurrence" ++ fnl () ++
+ str"cty: " ++ prc env_rhs evd c));
incr occ;
match occs with
| AtOccurrences occs ->
@@ -1458,10 +1448,10 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
| Unspecified prefer_abstraction ->
let evd, fixed, evty = set_holes env_rhs evd fixed cty subst in
let evty = nf_evar evd evty in
- if debug_ho_unification () then
- Feedback.msg_debug Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++
- str" of type: " ++ prc env_evar evd evty ++
- str " for " ++ prc env_rhs evd c);
+ debug_ho_unification (fun () ->
+ Pp.(str"abstracting one occurrence " ++ prc env_rhs evd inst ++
+ str" of type: " ++ prc env_evar evd evty ++
+ str " for " ++ prc env_rhs evd c));
let instance = Filter.filter_list filter instance in
(* Allow any type lower than the variable's type as the
abstracted subterm might have a smaller type, which could be
@@ -1477,8 +1467,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
evd, fixed, mkEvar (evk, instance)
in
let evd, fixed, rhs' = apply_on_subterm env_rhs evd fixed set_var test c rhs in
- if debug_ho_unification () then
- Feedback.msg_debug Pp.(str"abstracted: " ++ prc env_rhs evd rhs');
+ debug_ho_unification (fun () ->
+ Pp.(str"abstracted: " ++ prc env_rhs evd rhs'));
let () = check_selected_occs env_rhs evd c !occ occs in
let env_rhs' = push_named (NamedDecl.LocalAssum (id,idty)) env_rhs in
set_holes env_rhs' evd fixed rhs' subst
@@ -1491,9 +1481,9 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
(* Thin evars making the term typable in env_evar *)
let evd, rhs' = thin_evars env_evar evd ctxt rhs' in
(* We instantiate the evars of which the value is forced by typing *)
- if debug_ho_unification () then
- (Feedback.msg_debug Pp.(str"solve_evars on: " ++ prc env_evar evd rhs');
- Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
+ debug_ho_unification (fun () ->
+ Pp.(str"solve_evars on: " ++ prc env_evar evd rhs' ++ fnl () ++
+ str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
let evd,rhs' =
try !solve_evars env_evar evd rhs'
with e when Pretype_errors.precatchable_exception e ->
@@ -1501,18 +1491,18 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
raise (TypingFailed evd) in
let rhs' = nf_evar evd rhs' in
(* We instantiate the evars of which the value is forced by typing *)
- if debug_ho_unification () then
- (Feedback.msg_debug Pp.(str"after solve_evars: " ++ prc env_evar evd rhs');
- Feedback.msg_debug Pp.(str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
+ debug_ho_unification (fun () ->
+ Pp.(str"after solve_evars: " ++ prc env_evar evd rhs' ++ fnl () ++
+ str"evars: " ++ pr_evar_map (Some 0) env_evar evd));
let rec abstract_free_holes evd = function
| (id,idty,c,cty,evsref,_,_)::l ->
let id = id.binder_name in
let c = nf_evar evd c in
- if debug_ho_unification () then
- Feedback.msg_debug Pp.(str"abstracting: " ++
- prc env_rhs evd (mkVar id) ++ spc () ++
- prc env_rhs evd c);
+ debug_ho_unification (fun () ->
+ Pp.(str"abstracting: " ++
+ prc env_rhs evd (mkVar id) ++ spc () ++
+ prc env_rhs evd c));
let rec force_instantiation evd = function
| (evk,evty,inst,abstract)::evs ->
let evk = Option.default evk (Evarutil.advance evd evk) in
@@ -1541,14 +1531,14 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
with IllTypedInstance _ (* from instantiate_evar *) | TypingFailed _ ->
user_err (Pp.str "Cannot find an instance.")
else
- ((if debug_ho_unification () then
+ ((debug_ho_unification (fun () ->
let evi = Evd.find evd evk in
let env = Evd.evar_env env_rhs evi in
- Feedback.msg_debug Pp.(str"evar is defined: " ++
+ Pp.(str"evar is defined: " ++
int (Evar.repr evk) ++ spc () ++
prc env evd (match evar_body evi with Evar_defined c -> c
| Evar_empty -> assert false)));
- evd)
+ evd))
in force_instantiation evd evs
| [] -> abstract_free_holes evd l
in force_instantiation evd !evsref
@@ -1556,27 +1546,27 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
if Evd.is_defined evd evk then
(* Can happen due to dependencies: instantiating evars in the arguments of evk might
instantiate evk itself. *)
- (if debug_ho_unification () then
+ (debug_ho_unification (fun () ->
begin
let evi = Evd.find evd evk in
let evenv = evar_env env_rhs evi in
let body = match evar_body evi with Evar_empty -> assert false | Evar_defined c -> c in
- Feedback.msg_debug Pp.(str"evar was defined already as: " ++ prc evenv evd body)
- end;
+ Pp.(str"evar was defined already as: " ++ prc evenv evd body)
+ end);
evd)
else
try
let evi = Evd.find_undefined evd evk in
let evenv = evar_env env_rhs evi in
let rhs' = nf_evar evd rhs' in
- if debug_ho_unification () then
- Feedback.msg_debug Pp.(str"abstracted type before second solve_evars: " ++
- prc evenv evd rhs');
+ debug_ho_unification (fun () ->
+ Pp.(str"abstracted type before second solve_evars: " ++
+ prc evenv evd rhs'));
(* solve_evars is not commuting with nf_evar, because restricting
an evar might provide a more specific type. *)
let evd, _ = !solve_evars evenv evd rhs' in
- if debug_ho_unification () then
- Feedback.msg_debug Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs'));
+ debug_ho_unification (fun () ->
+ Pp.(str"abstracted type: " ++ prc evenv evd (nf_evar evd rhs')));
let flags = default_flags_of TransparentState.full in
Evarsolve.instantiate_evar evar_unify flags env_rhs evd evk rhs'
with IllTypedInstance _ -> raise (TypingFailed evd)
@@ -1629,11 +1619,10 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
let t2 = apprec_nohdbeta flags env evd (whd_head_evar evd t2) in
let (term1,l1 as appr1) = try destApp evd t1 with DestKO -> (t1, [||]) in
let (term2,l2 as appr2) = try destApp evd t2 with DestKO -> (t2, [||]) in
- let () = if debug_unification () then
- let open Pp in
- Feedback.msg_debug (v 0 (str "Heuristic:" ++ spc () ++
+ let () = debug_unification (fun () ->
+ Pp.(v 0 (str "Heuristic:" ++ spc () ++
Termops.Internal.print_constr_env env evd t1 ++ cut () ++
- Termops.Internal.print_constr_env env evd t2 ++ cut ())) in
+ Termops.Internal.print_constr_env env evd t2 ++ cut ()))) in
let app_empty = Array.is_empty l1 && Array.is_empty l2 in
match EConstr.kind evd term1, EConstr.kind evd term2 with
| Evar (evk1,args1), (Rel _|Var _) when app_empty
diff --git a/pretyping/inductiveops.ml b/pretyping/inductiveops.ml
index d02b015604..2e678f5700 100644
--- a/pretyping/inductiveops.ml
+++ b/pretyping/inductiveops.ml
@@ -347,37 +347,50 @@ let make_case_invert env (IndType (((ind,u),params),indices)) ci =
then CaseInvert {indices=Array.of_list indices}
else NoInvert
+let make_project env sigma ind pred c branches ps =
+ let open EConstr in
+ assert(Array.length branches == 1);
+ let na, ty, t = destLambda sigma pred in
+ let () =
+ let mib, _ = Inductive.lookup_mind_specif env ind in
+ if (* dependent *) not (Vars.noccurn sigma 1 t) &&
+ not (has_dependent_elim mib) then
+ user_err ~hdr:"make_case_or_project"
+ Pp.(str"Dependent case analysis not allowed" ++
+ str" on inductive type " ++ Termops.Internal.print_constr_env env sigma (mkInd ind))
+ in
+ let branch = branches.(0) in
+ let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in
+ let n, len, ctx =
+ List.fold_right
+ (fun decl (i, j, ctx) ->
+ match decl with
+ | LocalAssum (na, ty) ->
+ let t = mkProj (Projection.make ps.(i) true, mkRel j) in
+ (i + 1, j + 1, LocalDef (na, t, Vars.liftn 1 j ty) :: ctx)
+ | LocalDef (na, b, ty) ->
+ (i, j + 1, LocalDef (na, Vars.liftn 1 j b, Vars.liftn 1 j ty) :: ctx))
+ ctx (0, 1, [])
+ in
+ mkLetIn (na, c, ty, it_mkLambda_or_LetIn (Vars.liftn 1 (Array.length ps + 1) br) ctx)
+
+let simple_make_case_or_project env sigma ci pred invert c branches =
+ let open EConstr in
+ let ind = ci.ci_ind in
+ let projs = get_projections env ind in
+ match projs with
+ | None -> mkCase (EConstr.contract_case env sigma (ci, pred, invert, c, branches))
+ | Some ps -> make_project env sigma ind pred c branches ps
+
let make_case_or_project env sigma indt ci pred c branches =
let open EConstr in
let IndType (((ind,_),_),_) = indt in
let projs = get_projections env ind in
match projs with
- | None -> (mkCase (EConstr.contract_case env sigma (ci, pred, make_case_invert env indt ci, c, branches)))
- | Some ps ->
- assert(Array.length branches == 1);
- let na, ty, t = destLambda sigma pred in
- let () =
- let mib, _ = Inductive.lookup_mind_specif env ind in
- if (* dependent *) not (Vars.noccurn sigma 1 t) &&
- not (has_dependent_elim mib) then
- user_err ~hdr:"make_case_or_project"
- Pp.(str"Dependent case analysis not allowed" ++
- str" on inductive type " ++ Termops.Internal.print_constr_env env sigma (mkInd ind))
- in
- let branch = branches.(0) in
- let ctx, br = decompose_lam_n_assum sigma (Array.length ps) branch in
- let n, len, ctx =
- List.fold_right
- (fun decl (i, j, ctx) ->
- match decl with
- | LocalAssum (na, ty) ->
- let t = mkProj (Projection.make ps.(i) true, mkRel j) in
- (i + 1, j + 1, LocalDef (na, t, Vars.liftn 1 j ty) :: ctx)
- | LocalDef (na, b, ty) ->
- (i, j + 1, LocalDef (na, Vars.liftn 1 j b, Vars.liftn 1 j ty) :: ctx))
- ctx (0, 1, [])
- in
- mkLetIn (na, c, ty, it_mkLambda_or_LetIn (Vars.liftn 1 (Array.length ps + 1) br) ctx)
+ | None ->
+ let invert = make_case_invert env indt ci in
+ mkCase (EConstr.contract_case env sigma (ci, pred, invert, c, branches))
+ | Some ps -> make_project env sigma ind pred c branches ps
(* substitution in a signature *)
diff --git a/pretyping/inductiveops.mli b/pretyping/inductiveops.mli
index 8e83814fa0..59ef8e08e3 100644
--- a/pretyping/inductiveops.mli
+++ b/pretyping/inductiveops.mli
@@ -212,6 +212,12 @@ val make_case_or_project :
env -> evar_map -> inductive_type -> case_info ->
(* pred *) EConstr.constr -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr
+(** Sometimes [make_case_or_project] is nicer to call with a pre-built
+ [case_invert] than [inductive_type]. *)
+val simple_make_case_or_project :
+ env -> evar_map -> case_info ->
+ (* pred *) EConstr.constr -> EConstr.case_invert -> (* term *) EConstr.constr -> (* branches *) EConstr.constr array -> EConstr.constr
+
val make_case_invert : env -> inductive_type -> case_info
-> EConstr.case_invert
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 55ff91327a..b19dbd46be 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -470,15 +470,15 @@ let start_profiler_linux profile_fn =
Unix.stdin dev_null dev_null
in
(* doesn't seem to be a way to test whether process creation succeeded *)
- if !Flags.debug then
- Feedback.msg_debug (Pp.str (Format.sprintf "Native compute profiler started, pid = %d, output to: %s" profiler_pid profile_fn));
+ debug_native_compiler (fun () ->
+ Pp.str (Format.sprintf "Native compute profiler started, pid = %d, output to: %s" profiler_pid profile_fn));
Some profiler_pid
(* kill profiler via SIGINT *)
let stop_profiler_linux m_pid =
match m_pid with
| Some pid -> (
- let _ = if !Flags.debug then Feedback.msg_debug (Pp.str "Stopping native code profiler") in
+ let _ = debug_native_compiler (fun () -> Pp.str "Stopping native code profiler") in
try
Unix.kill pid Sys.sigint;
let _ = Unix.waitpid [] pid in ()
@@ -503,15 +503,9 @@ let stop_profiler m_pid =
| _ -> ()
let native_norm env sigma c ty =
+ Nativelib.link_libraries ();
let c = EConstr.Unsafe.to_constr c in
let ty = EConstr.Unsafe.to_constr ty in
- if not (Flags.get_native_compiler ()) then
- user_err Pp.(str "Native_compute reduction has been disabled.")
- else
- (*
- Format.eprintf "Numbers of free variables (named): %i\n" (List.length vl1);
- Format.eprintf "Numbers of free variables (rel): %i\n" (List.length vl2);
- *)
let profile = get_profiling_enabled () in
let print_timing = get_timing_enabled () in
let ml_filename, prefix = Nativelib.get_ml_filename () in
@@ -527,17 +521,22 @@ let native_norm env sigma c ty =
if print_timing then Feedback.msg_info (Pp.str time_info);
let profiler_pid = if profile then start_profiler () else None in
let t0 = Unix.gettimeofday () in
- Nativelib.call_linker ~fatal:true ~prefix fn (Some upd);
+ let (rt1, _) = Nativelib.execute_library ~prefix fn upd in
let t1 = Unix.gettimeofday () in
if profile then stop_profiler profiler_pid;
let time_info = Format.sprintf "native_compute: Evaluation done in %.5f" (t1 -. t0) in
if print_timing then Feedback.msg_info (Pp.str time_info);
- let res = nf_val env sigma !Nativelib.rt1 ty in
+ let res = nf_val env sigma rt1 ty in
let t2 = Unix.gettimeofday () in
let time_info = Format.sprintf "native_compute: Reification done in %.5f" (t2 -. t1) in
if print_timing then Feedback.msg_info (Pp.str time_info);
EConstr.of_constr res
+let native_norm env sigma c ty =
+ if not (Flags.get_native_compiler ()) then
+ user_err Pp.(str "Native_compute reduction has been disabled.");
+ native_norm env sigma c ty
+
let native_conv_generic pb sigma t =
Nativeconv.native_conv_gen pb (evars_of_evar_map sigma) t
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index e86a8a28c9..3ccc6ea125 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1398,7 +1398,7 @@ let understand_ltac flags env sigma lvar kind c =
let (sigma, c, _) = ise_pretype_gen flags env sigma lvar kind c in
(sigma, c)
-let path_convertible env sigma i p q =
+let path_convertible env sigma cl p q =
let open Coercionops in
let mkGRef ref = DAst.make @@ Glob_term.GRef(ref,None) in
let mkGVar id = DAst.make @@ Glob_term.GVar(id) in
@@ -1423,7 +1423,7 @@ let path_convertible env sigma i p q =
p'
| [] ->
(* identity function for the class [i]. *)
- let cl,params = class_info_from_index i in
+ let params = (class_info cl).cl_param in
let clty =
match cl with
| CL_SORT -> mkGSort (Glob_term.UAnonymous {rigid=false})
@@ -1434,8 +1434,7 @@ let path_convertible env sigma i p q =
| CL_PROJ p -> mkGRef (GlobRef.ConstRef (Projection.Repr.constant p))
in
let names =
- List.init params.cl_param
- (fun n -> Id.of_string ("x" ^ string_of_int n))
+ List.init params (fun n -> Id.of_string ("x" ^ string_of_int n))
in
List.fold_right
(fun id t -> mkGLambda (Name id, mkGHole (), t)) names @@
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 54a47a252d..4083d3bc23 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -686,11 +686,7 @@ module CredNative = RedNative(CNativeEntries)
contract_* in any case .
*)
-let debug_RAKAM =
- Goptions.declare_bool_option_and_ref
- ~depr:false
- ~key:["Debug";"RAKAM"]
- ~value:false
+let debug_RAKAM = CDebug.create ~name:"RAKAM" ()
let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) =
let args = Stack.tail ci.ci_npar args in
@@ -709,18 +705,18 @@ let apply_branch env sigma (ind, i) args (ci, u, pms, iv, r, lf) =
let rec whd_state_gen flags env sigma =
let open Context.Named.Declaration in
let rec whrec (x, stack) : state =
- let () = if debug_RAKAM () then
+ let () =
let open Pp in
let pr c = Termops.Internal.print_constr_env env sigma c in
- Feedback.msg_debug
+ debug_RAKAM (fun () ->
(h (str "<<" ++ pr x ++
str "|" ++ cut () ++ Stack.pr pr stack ++
- str ">>"))
+ str ">>")))
in
let c0 = EConstr.kind sigma x in
let fold () =
- let () = if debug_RAKAM () then
- let open Pp in Feedback.msg_debug (str "<><><><><>") in
+ let () = debug_RAKAM (fun () ->
+ let open Pp in str "<><><><><>") in
((EConstr.of_kind c0, stack))
in
match c0 with
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 41d16f1c3c..09bcc860d0 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -19,7 +19,7 @@ open Environ
exception Elimconst
-val debug_RAKAM : unit -> bool
+val debug_RAKAM : CDebug.t
module CredNative : Primred.RedNative with
type elem = EConstr.t and type args = EConstr.t array and type evd = Evd.evar_map
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 430813e874..4e89018656 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1203,9 +1203,7 @@ let unfoldn loccname env sigma c =
(* Re-folding constants tactics: refold com in term c *)
let fold_one_com com env sigma c =
- let rcom =
- try red_product env sigma com
- with Redelimination -> user_err Pp.(str "Not reducible.") in
+ let rcom = red_product env sigma com in
(* Reason first on the beta-iota-zeta normal form of the constant as
unfold produces it, so that the "unfold f; fold f" configuration works
to refold fix expressions *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 83e46e3295..df0f49a033 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -49,11 +49,7 @@ let is_keyed_unification =
~key:["Keyed";"Unification"]
~value:false
-let debug_unification =
- Goptions.declare_bool_option_and_ref
- ~depr:false
- ~key:["Debug";"Tactic";"Unification"]
- ~value:false
+let debug_tactic_unification = CDebug.create ~name:"tactic-unification" ()
(** Making this unification algorithm correct w.r.t. the evar-map abstraction
breaks too much stuff. So we redefine incorrect functions here. *)
@@ -713,8 +709,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
let cM = Evarutil.whd_head_evar sigma curm
and cN = Evarutil.whd_head_evar sigma curn in
let () =
- if debug_unification () then
- Feedback.msg_debug (
+ debug_tactic_unification (fun () ->
Termops.Internal.print_constr_env curenv sigma cM ++ str" ~= " ++
Termops.Internal.print_constr_env curenv sigma cN)
in
@@ -1138,7 +1133,7 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
in
- if debug_unification () then Feedback.msg_debug (str "Starting unification");
+ debug_tactic_unification (fun () -> str "Starting unification");
let opt = { at_top = conv_at_top; with_types = false; with_cs = true } in
try
let res =
@@ -1165,11 +1160,11 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
let a = match res with
| Some sigma -> sigma, ms, es
| None -> unirec_rec (env,0) cv_pb opt subst (fst m) (fst n) in
- if debug_unification () then Feedback.msg_debug (str "Leaving unification with success");
+ debug_tactic_unification (fun () -> str "Leaving unification with success");
a
with e ->
let e = Exninfo.capture e in
- if debug_unification () then Feedback.msg_debug (str "Leaving unification with failure");
+ debug_tactic_unification (fun () -> str "Leaving unification with failure");
Exninfo.iraise e
let unify_0 env sigma pb flags c1 c2 =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 16:12:20 +0000