aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/classops.ml34
-rw-r--r--pretyping/classops.mli2
-rw-r--r--pretyping/constr_matching.ml91
-rw-r--r--pretyping/constr_matching.mli23
-rw-r--r--pretyping/evarconv.ml4
-rw-r--r--pretyping/reductionops.ml117
-rw-r--r--pretyping/reductionops.mli4
-rw-r--r--pretyping/retyping.ml4
-rw-r--r--pretyping/tacred.ml4
-rw-r--r--pretyping/typeclasses.ml4
-rw-r--r--pretyping/unification.ml10
11 files changed, 110 insertions, 187 deletions
diff --git a/pretyping/classops.ml b/pretyping/classops.ml
index c36630f5d3..6d5ee504e5 100644
--- a/pretyping/classops.ml
+++ b/pretyping/classops.ml
@@ -322,16 +322,16 @@ let coercion_value { coe_value = c; coe_type = t; coe_context = ctx;
(* pretty-print functions are now in Pretty *)
(* rajouter une coercion dans le graphe *)
-let path_printer = ref (fun _ -> str "<a class path>"
- : (Bijint.Index.t * Bijint.Index.t) * inheritance_path -> Pp.t)
+let path_printer : (env -> Evd.evar_map -> (Bijint.Index.t * Bijint.Index.t) * 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 print_path env sigma x = !path_printer env sigma x
-let message_ambig l =
- (str"Ambiguous paths:" ++ spc () ++
- prlist_with_sep fnl (fun ijp -> print_path ijp) l)
+let message_ambig env sigma l =
+ str"Ambiguous paths:" ++ spc () ++
+ prlist_with_sep fnl (fun ijp -> print_path env sigma ijp) l
(* add_coercion_in_graph : coe_index * cl_index * cl_index -> unit
coercion,source,target *)
@@ -344,8 +344,8 @@ let different_class_params i =
| CL_IND i -> Global.is_polymorphic (IndRef i)
| CL_CONST c -> Global.is_polymorphic (ConstRef c)
| _ -> false
-
-let add_coercion_in_graph (ic,source,target) =
+
+let add_coercion_in_graph env sigma (ic,source,target) =
let old_inheritance_graph = !inheritance_graph in
let ambig_paths =
(ref [] : ((cl_index * cl_index) * inheritance_path) list ref) in
@@ -387,7 +387,7 @@ let add_coercion_in_graph (ic,source,target) =
end;
let is_ambig = match !ambig_paths with [] -> false | _ -> true in
if is_ambig && not !Flags.quiet then
- Feedback.msg_info (message_ambig !ambig_paths)
+ Feedback.msg_info (message_ambig env sigma !ambig_paths)
type coercion = {
coercion_type : coe_typ;
@@ -433,13 +433,13 @@ let _ =
optread = (fun () -> !automatically_import_coercions);
optwrite = (:=) automatically_import_coercions }
-let cache_coercion (_, c) =
+let cache_coercion env sigma (_, c) =
let () = add_class c.coercion_source in
let () = add_class c.coercion_target in
let is, _ = class_info c.coercion_source in
let it, _ = class_info c.coercion_target in
- let value, ctx = Universes.fresh_global_instance (Global.env()) c.coercion_type in
- let typ = Retyping.get_type_of (Global.env ()) Evd.empty (EConstr.of_constr value) in
+ let value, ctx = Universes.fresh_global_instance env c.coercion_type in
+ let typ = Retyping.get_type_of env sigma (EConstr.of_constr value) in
let typ = EConstr.Unsafe.to_constr typ in
let xf =
{ coe_value = value;
@@ -450,15 +450,15 @@ let cache_coercion (_, c) =
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 (xf,is,it)
+ add_coercion_in_graph env sigma (xf,is,it)
let load_coercion _ o =
if !automatically_import_coercions then
- cache_coercion o
+ cache_coercion (Global.env ()) Evd.empty o
let open_coercion i o =
if Int.equal i 1 && not !automatically_import_coercions then
- cache_coercion o
+ cache_coercion (Global.env ()) Evd.empty o
let subst_coercion (subst, c) =
let coe = subst_coe_typ subst c.coercion_type in
@@ -497,7 +497,9 @@ let inCoercion : coercion -> obj =
declare_object {(default_object "COERCION") with
open_function = open_coercion;
load_function = load_coercion;
- cache_function = cache_coercion;
+ cache_function = (fun objn ->
+ let env = Global.env () in cache_coercion env Evd.empty objn
+ );
subst_function = subst_coercion;
classify_function = classify_coercion;
discharge_function = discharge_coercion }
diff --git a/pretyping/classops.mli b/pretyping/classops.mli
index b41d0efac5..47b41f17b2 100644
--- a/pretyping/classops.mli
+++ b/pretyping/classops.mli
@@ -96,7 +96,7 @@ val lookup_pattern_path_between :
(**/**)
(* Crade *)
val install_path_printer :
- ((cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
+ (env -> evar_map -> (cl_index * cl_index) * inheritance_path -> Pp.t) -> unit
(**/**)
(** {6 This is for printing purpose } *)
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 20ef65c884..ec7c3077fb 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -13,7 +13,6 @@ open Util
open Names
open Globnames
open Termops
-open Reductionops
open Term
open EConstr
open Vars
@@ -207,7 +206,7 @@ let merge_binding sigma allow_bound_rels ctx n cT subst =
in
constrain sigma n c subst
-let matches_core env sigma convert allow_partial_app allow_bound_rels
+let matches_core env sigma allow_bound_rels
(binding_vars,pat) c =
let open EConstr in
let convref ref c =
@@ -216,11 +215,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
| ConstRef c, Const (c',_) -> Constant.equal c c'
| IndRef i, Ind (i', _) -> Names.eq_ind i i'
| ConstructRef c, Construct (c',u) -> Names.eq_constructor c c'
- | _, _ ->
- (if convert then
- let sigma,c' = Evd.fresh_global env sigma ref in
- is_conv env sigma (EConstr.of_constr c') c
- else false)
+ | _, _ -> false
in
let rec sorec ctx env subst p t =
let cT = strip_outer_cast sigma t in
@@ -265,7 +260,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
| PApp (PApp (h, a1), a2), _ ->
sorec ctx env subst (PApp(h,Array.append a1 a2)) t
- | PApp (PMeta meta,args1), App (c2,args2) when allow_partial_app ->
+ | PApp (PMeta meta,args1), App (c2,args2) ->
(let diff = Array.length args2 - Array.length args1 in
if diff >= 0 then
let args21, args22 = Array.chop diff args2 in
@@ -378,14 +373,14 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
in
sorec [] env (Id.Map.empty, Id.Map.empty) pat c
-let matches_core_closed env sigma convert allow_partial_app pat c =
- let names, subst = matches_core env sigma convert allow_partial_app false pat c in
+let matches_core_closed env sigma pat c =
+ let names, subst = matches_core env sigma false pat c in
(names, Id.Map.map snd subst)
-let extended_matches env sigma = matches_core env sigma false true true
+let extended_matches env sigma = matches_core env sigma true
let matches env sigma pat c =
- snd (matches_core_closed env sigma false true (Id.Set.empty,pat) c)
+ snd (matches_core_closed env sigma (Id.Set.empty,pat) c)
let special_meta = (-1)
@@ -410,9 +405,9 @@ let matches_head env sigma pat c =
matches env sigma pat head
(* Tells if it is an authorized occurrence and if the instance is closed *)
-let authorized_occ env sigma partial_app closed pat c mk_ctx =
+let authorized_occ env sigma closed pat c mk_ctx =
try
- let subst = matches_core_closed env sigma false partial_app pat c in
+ let subst = matches_core_closed env sigma pat c in
if closed && Id.Map.exists (fun _ c -> not (closed0 sigma c)) (snd subst)
then (fun next -> next ())
else (fun next -> mkresult subst (mk_ctx (mkMeta special_meta)) next)
@@ -421,10 +416,10 @@ let authorized_occ env sigma partial_app closed pat c mk_ctx =
let subargs env v = Array.map_to_list (fun c -> (env, c)) v
(* Tries to match a subterm of [c] with [pat] *)
-let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
+let sub_match ?(closed=true) env sigma pat c =
let open EConstr in
let rec aux env c mk_ctx next =
- let here = authorized_occ env sigma partial_app closed pat c mk_ctx in
+ let here = authorized_occ env sigma closed pat c mk_ctx in
let next () = match EConstr.kind sigma c with
| Cast (c1,k,c2) ->
let next_mk_ctx = function
@@ -454,34 +449,12 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
let env' = EConstr.push_rel (LocalDef (x,c1,t)) env in
try_aux [(env, c1); (env', c2)] next_mk_ctx next
| App (c1,lc) ->
- let topdown = true in
- if partial_app then
- if topdown then
- let lc1 = Array.sub lc 0 (Array.length lc - 1) in
- let app = mkApp (c1,lc1) in
- let mk_ctx = function
- | [app';c] -> mk_ctx (mkApp (app',[|c|]))
- | _ -> assert false in
- try_aux [(env, app); (env, Array.last lc)] mk_ctx next
- else
- let rec aux2 app args next =
- match args with
- | [] ->
- let mk_ctx le =
- mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
- let sub = (env, c1) :: subargs env lc in
- try_aux sub mk_ctx next
- | arg :: args ->
- let app = mkApp (app,[|arg|]) in
- let next () = aux2 app args next in
- let mk_ctx ce = mk_ctx (mkApp (ce, Array.of_list args)) in
- aux env app mk_ctx next in
- aux2 c1 (Array.to_list lc) next
- else
- let mk_ctx le =
- mk_ctx (mkApp (List.hd le, Array.of_list (List.tl le))) in
- let sub = (env, c1) :: subargs env lc in
- try_aux sub mk_ctx next
+ let lc1 = Array.sub lc 0 (Array.length lc - 1) in
+ let app = mkApp (c1,lc1) in
+ let mk_ctx = function
+ | [app';c] -> mk_ctx (mkApp (app',[|c|]))
+ | _ -> assert false in
+ try_aux [(env, app); (env, Array.last lc)] mk_ctx next
| Case (ci,hd,c1,lc) ->
let next_mk_ctx = function
| c1 :: hd :: lc -> mk_ctx (mkCase (ci,hd,c1,Array.of_list lc))
@@ -504,14 +477,11 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
let sub = subargs env types @ subargs env bodies in
try_aux sub next_mk_ctx next
| Proj (p,c') ->
- let next_mk_ctx le = mk_ctx (mkProj (p,List.hd le)) in
- if partial_app then
- try
- let term = Retyping.expand_projection env sigma p c' [] in
- aux env term mk_ctx next
- with Retyping.RetypeError _ -> next ()
- else
- try_aux [env, c'] next_mk_ctx next
+ begin try
+ let term = Retyping.expand_projection env sigma p c' [] in
+ aux env term mk_ctx next
+ with Retyping.RetypeError _ -> next ()
+ end
| Construct _| Ind _|Evar _|Const _ | Rel _|Meta _|Var _|Sort _ ->
next ()
in
@@ -532,13 +502,7 @@ let sub_match ?(partial_app=false) ?(closed=true) env sigma pat c =
let result () = aux env c (fun x -> x) lempty in
IStream.thunk result
-let match_subterm env sigma pat c = sub_match env sigma (Id.Set.empty,pat) c
-
-let match_appsubterm env sigma pat c =
- sub_match ~partial_app:true env sigma (Id.Set.empty,pat) c
-
-let match_subterm_gen env sigma app pat c =
- sub_match ~partial_app:app env sigma pat c
+let match_subterm env sigma pat c = sub_match env sigma pat c
let is_matching env sigma pat c =
try let _ = matches env sigma pat c in true
@@ -550,12 +514,5 @@ let is_matching_head env sigma pat c =
let is_matching_appsubterm ?(closed=true) env sigma pat c =
let pat = (Id.Set.empty,pat) in
- let results = sub_match ~partial_app:true ~closed env sigma pat c in
+ let results = sub_match ~closed env sigma pat c in
not (IStream.is_empty results)
-
-let matches_conv env sigma p c =
- snd (matches_core_closed env sigma true false (Id.Set.empty,p) c)
-
-let is_matching_conv env sigma pat n =
- try let _ = matches_conv env sigma pat n in true
- with PatternMatchingFailure -> false
diff --git a/pretyping/constr_matching.mli b/pretyping/constr_matching.mli
index 780ccc23d1..e4d9ff9e1e 100644
--- a/pretyping/constr_matching.mli
+++ b/pretyping/constr_matching.mli
@@ -55,38 +55,19 @@ val is_matching : env -> Evd.evar_map -> constr_pattern -> constr -> bool
prefix of it matches against [pat] *)
val is_matching_head : env -> Evd.evar_map -> constr_pattern -> constr -> bool
-(** [matches_conv env sigma] matches up to conversion in environment
- [(env,sigma)] when constants in pattern are concerned; it raises
- [PatternMatchingFailure] if not matchable; bindings are given in
- increasing order based on the numbers given in the pattern *)
-val matches_conv : env -> Evd.evar_map -> constr_pattern -> constr -> patvar_map
-
(** The type of subterm matching results: a substitution + a context
(whose hole is denoted here with [special_meta]) *)
type matching_result =
{ m_sub : bound_ident_map * patvar_map;
m_ctx : EConstr.t }
-(** [match_subterm n pat c] returns the substitution and the context
- corresponding to each **closed** subterm of [c] matching [pat]. *)
-val match_subterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t
-
-(** [match_appsubterm pat c] returns the substitution and the context
+(** [match_subterm pat c] returns the substitution and the context
corresponding to each **closed** subterm of [c] matching [pat],
considering application contexts as well. *)
-val match_appsubterm : env -> Evd.evar_map -> constr_pattern -> constr -> matching_result IStream.t
-
-(** [match_subterm_gen] calls either [match_subterm] or [match_appsubterm] *)
-val match_subterm_gen : env -> Evd.evar_map ->
- bool (** true = with app context *) ->
+val match_subterm : env -> Evd.evar_map ->
binding_bound_vars * constr_pattern -> constr ->
matching_result IStream.t
(** [is_matching_appsubterm pat c] tells if a subterm of [c] matches
against [pat] taking partial subterms into consideration *)
val is_matching_appsubterm : ?closed:bool -> env -> Evd.evar_map -> constr_pattern -> constr -> bool
-
-(** [is_matching_conv env sigma pat c] tells if [c] matches against [pat]
- up to conversion for constants in patterns *)
-val is_matching_conv :
- env -> Evd.evar_map -> constr_pattern -> constr -> bool
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index e5776d2eca..cb88446236 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -1063,8 +1063,8 @@ let evar_conv_x ts = evar_conv_x (ts, true)
(* Profiling *)
let evar_conv_x =
if Flags.profile then
- let evar_conv_xkey = Profile.declare_profile "evar_conv_x" in
- Profile.profile6 evar_conv_xkey evar_conv_x
+ let evar_conv_xkey = CProfile.declare_profile "evar_conv_x" in
+ CProfile.profile6 evar_conv_xkey evar_conv_x
else evar_conv_x
let evar_conv_hook_get, evar_conv_hook_set = Hook.make ~default:evar_conv_x ()
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 2f8e5b9643..ac88468545 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -294,12 +294,12 @@ sig
val append_app : 'a array -> 'a t -> 'a t
val decomp : 'a t -> ('a * 'a t) option
val decomp_node_last : 'a app_node -> 'a t -> ('a * 'a t)
- val equal : ('a * int -> 'a * int -> bool) -> (('a, 'a) pfixpoint * int -> ('a, 'a) pfixpoint * int -> bool)
- -> 'a t -> 'a t -> (int * int) option
+ val equal : ('a -> 'a -> bool) -> (('a, 'a) pfixpoint -> ('a, 'a) pfixpoint -> bool)
+ -> 'a t -> 'a t -> bool
val compare_shape : 'a t -> 'a t -> bool
val map : ('a -> 'a) -> 'a t -> 'a t
val fold2 : ('a -> constr -> constr -> 'a) -> 'a ->
- constr t -> constr t -> 'a * int * int
+ constr t -> constr t -> 'a
val append_app_list : 'a list -> 'a t -> 'a t
val strip_app : 'a t -> 'a t * 'a t
val strip_n_app : int -> 'a t -> ('a t * 'a * 'a t) option
@@ -397,44 +397,37 @@ struct
else (l.(j), sk)
let equal f f_fix sk1 sk2 =
- let equal_cst_member x lft1 y lft2 =
+ let equal_cst_member x y =
match x, y with
| Cst_const (c1,u1), Cst_const (c2, u2) ->
- Constant.equal c1 c2 && Univ.Instance.equal u1 u2
+ Constant.equal c1 c2 && Univ.Instance.equal u1 u2
| Cst_proj p1, Cst_proj p2 ->
- Constant.equal (Projection.constant p1) (Projection.constant p2)
+ Constant.equal (Projection.constant p1) (Projection.constant p2)
| _, _ -> false
in
- let rec equal_rec sk1 lft1 sk2 lft2 =
+ let rec equal_rec sk1 sk2 =
match sk1,sk2 with
- | [],[] -> Some (lft1,lft2)
+ | [],[] -> true
| App a1 :: s1, App a2 :: s2 ->
- let t1,s1' = decomp_node_last a1 s1 in
- let t2,s2' = decomp_node_last a2 s2 in
- if f (t1,lft1) (t2,lft2) then equal_rec s1' lft1 s2' lft2 else None
+ let t1,s1' = decomp_node_last a1 s1 in
+ let t2,s2' = decomp_node_last a2 s2 in
+ (f t1 t2) && (equal_rec s1' s2')
| Case (_,t1,a1,_) :: s1, Case (_,t2,a2,_) :: s2 ->
- if f (t1,lft1) (t2,lft2) && CArray.equal (fun x y -> f (x,lft1) (y,lft2)) a1 a2
- then equal_rec s1 lft1 s2 lft2
- else None
+ f t1 t2 && CArray.equal (fun x y -> f x y) a1 a2 && equal_rec s1 s2
| (Proj (n1,m1,p,_)::s1, Proj(n2,m2,p2,_)::s2) ->
- if Int.equal n1 n2 && Int.equal m1 m2
- && Constant.equal (Projection.constant p) (Projection.constant p2)
- then equal_rec s1 lft1 s2 lft2
- else None
+ Int.equal n1 n2 && Int.equal m1 m2
+ && Constant.equal (Projection.constant p) (Projection.constant p2)
+ && equal_rec s1 s2
| Fix (f1,s1,_) :: s1', Fix (f2,s2,_) :: s2' ->
- if f_fix (f1,lft1) (f2,lft2) then
- match equal_rec (List.rev s1) lft1 (List.rev s2) lft2 with
- | None -> None
- | Some (lft1',lft2') -> equal_rec s1' lft1' s2' lft2'
- else None
+ f_fix f1 f2
+ && equal_rec (List.rev s1) (List.rev s2)
+ && equal_rec s1' s2'
| Cst (c1,curr1,remains1,params1,_)::s1', Cst (c2,curr2,remains2,params2,_)::s2' ->
- if equal_cst_member c1 lft1 c2 lft2 then
- match equal_rec (List.rev params1) lft1 (List.rev params2) lft2 with
- | Some (lft1',lft2') -> equal_rec s1' lft1' s2' lft2'
- | None -> None
- else None
- | ((App _|Case _|Proj _|Fix _|Cst _)::_|[]), _ -> None
- in equal_rec (List.rev sk1) 0 (List.rev sk2) 0
+ equal_cst_member c1 c2
+ && equal_rec (List.rev params1) (List.rev params2)
+ && equal_rec s1' s2'
+ | ((App _|Case _|Proj _|Fix _|Cst _)::_|[]), _ -> false
+ in equal_rec (List.rev sk1) (List.rev sk2)
let compare_shape stk1 stk2 =
let rec compare_rec bal stk1 stk2 =
@@ -455,34 +448,26 @@ struct
exception IncompatibleFold2
let fold2 f o sk1 sk2 =
- let rec aux o lft1 sk1 lft2 sk2 =
- let fold_array =
- Array.fold_left2 (fun a x y -> f a (Vars.lift lft1 x) (Vars.lift lft2 y))
- in
+ let rec aux o sk1 sk2 =
match sk1,sk2 with
- | [], [] -> o,lft1,lft2
+ | [], [] -> o
| App n1 :: q1, App n2 :: q2 ->
- let t1,l1 = decomp_node_last n1 q1 in
- let t2,l2 = decomp_node_last n2 q2 in
- aux (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2))
- lft1 l1 lft2 l2
+ let t1,l1 = decomp_node_last n1 q1 in
+ let t2,l2 = decomp_node_last n2 q2 in
+ aux (f o t1 t2) l1 l2
| Case (_,t1,a1,_) :: q1, Case (_,t2,a2,_) :: q2 ->
- aux (fold_array
- (f o (Vars.lift lft1 t1) (Vars.lift lft2 t2))
- a1 a2) lft1 q1 lft2 q2
+ aux (Array.fold_left2 f (f o t1 t2) a1 a2) q1 q2
| Proj (n1,m1,p1,_) :: q1, Proj (n2,m2,p2,_) :: q2 ->
- aux o lft1 q1 lft2 q2
+ aux o q1 q2
| Fix ((_,(_,a1,b1)),s1,_) :: q1, Fix ((_,(_,a2,b2)),s2,_) :: q2 ->
- let (o',lft1',lft2') = aux (fold_array (fold_array o b1 b2) a1 a2)
- lft1 (List.rev s1) lft2 (List.rev s2) in
- aux o' lft1' q1 lft2' q2
+ let o' = aux (Array.fold_left2 f (Array.fold_left2 f o b1 b2) a1 a2) (List.rev s1) (List.rev s2) in
+ aux o' q1 q2
| Cst (cst1,_,_,params1,_) :: q1, Cst (cst2,_,_,params2,_) :: q2 ->
- let (o',lft1',lft2') =
- aux o lft1 (List.rev params1) lft2 (List.rev params2)
- in aux o' lft1' q1 lft2' q2
+ let o' = aux o (List.rev params1) (List.rev params2) in
+ aux o' q1 q2
| (((App _|Case _|Proj _|Fix _| Cst _) :: _|[]), _) ->
- raise IncompatibleFold2
- in aux o 0 (List.rev sk1) 0 (List.rev sk2)
+ raise IncompatibleFold2
+ in aux o (List.rev sk1) (List.rev sk2)
let rec map f x = List.map (function
| (Proj (_,_,_,_)) as e -> e
@@ -535,12 +520,12 @@ struct
let list_of_app_stack s =
let rec aux = function
| App (i,a,j) :: s ->
- let (k,(args',s')) = aux s in
- let a' = Array.map (Vars.lift k) (Array.sub a i (j - i + 1)) in
- k,(Array.fold_right (fun x y -> x::y) a' args', s')
- | s -> (0,([],s)) in
- let (lft,(out,s')) = aux s in
- let init = match s' with [] when Int.equal lft 0 -> true | _ -> false in
+ let (args',s') = aux s in
+ let a' = Array.sub a i (j - i + 1) in
+ (Array.fold_right (fun x y -> x::y) a' args', s')
+ | s -> ([],s) in
+ let (out,s') = aux s in
+ let init = match s' with [] -> true | _ -> false in
Option.init init out
let assign s p c =
@@ -845,11 +830,9 @@ let _ = Goptions.declare_bool_option {
}
let equal_stacks sigma (x, l) (y, l') =
- let f_equal (x,lft1) (y,lft2) = eq_constr sigma (Vars.lift lft1 x) (Vars.lift lft2 y) in
- let eq_fix (a,b) (c,d) = f_equal (mkFix a, b) (mkFix c, d) in
- match Stack.equal f_equal eq_fix l l' with
- | None -> false
- | Some (lft1,lft2) -> f_equal (x, lft1) (y, lft2)
+ let f_equal x y = eq_constr sigma x y in
+ let eq_fix a b = f_equal (mkFix a) (mkFix b) in
+ Stack.equal f_equal eq_fix l l' && f_equal x y
let rec whd_state_gen ?csts ~refold ~tactic_mode flags env sigma =
let open Context.Named.Declaration in
@@ -1269,11 +1252,11 @@ let nf_all env sigma =
(* Conversion *)
(********************************************************************)
(*
-let fkey = Profile.declare_profile "fhnf";;
-let fhnf info v = Profile.profile2 fkey fhnf info v;;
+let fkey = CProfile.declare_profile "fhnf";;
+let fhnf info v = CProfile.profile2 fkey fhnf info v;;
-let fakey = Profile.declare_profile "fhnf_apply";;
-let fhnf_apply info k h a = Profile.profile4 fakey fhnf_apply info k h a;;
+let fakey = CProfile.declare_profile "fhnf_apply";;
+let fhnf_apply info k h a = CProfile.profile4 fakey fhnf_apply info k h a;;
*)
let is_transparent e k =
@@ -1283,7 +1266,7 @@ let is_transparent e k =
(* Conversion utility functions *)
-type conversion_test = constraints -> constraints
+type conversion_test = Constraint.t -> Constraint.t
let pb_is_equal pb = pb == Reduction.CONV
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 34fdbe8583..a277864c92 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -100,7 +100,7 @@ module Stack : sig
@return the result and the lifts to apply on the terms
@raise IncompatibleFold2 when [sk1] and [sk2] have incompatible shapes *)
val fold2 : ('a -> constr -> constr -> 'a) -> 'a ->
- constr t -> constr t -> 'a * int * int
+ constr t -> constr t -> 'a
val map : ('a -> 'a) -> 'a t -> 'a t
val append_app_list : 'a list -> 'a t -> 'a t
@@ -260,7 +260,7 @@ val is_transparent : Environ.env -> Constant.t tableKey -> bool
(** {6 Conversion Functions (uses closures, lazy strategy) } *)
-type conversion_test = constraints -> constraints
+type conversion_test = Constraint.t -> Constraint.t
val pb_is_equal : conv_pb -> bool
val pb_equal : conv_pb -> conv_pb
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index f8f086fad3..00b175c486 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -227,8 +227,8 @@ let type_of_global_reference_knowing_conclusion env sigma c conclty =
(* let f,_,_,_ = retype ~polyprop sigma in *)
(* if lax then f env c else anomaly_on_error (f env) c *)
-(* let get_type_of_key = Profile.declare_profile "get_type_of" *)
-(* let get_type_of = Profile.profile5 get_type_of_key get_type_of *)
+(* let get_type_of_key = CProfile.declare_profile "get_type_of" *)
+(* let get_type_of = CProfile.profile5 get_type_of_key get_type_of *)
(* let get_type_of ?(polyprop=true) ?(lax=false) env sigma c = *)
(* get_type_of polyprop lax env sigma c *)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 85383ba398..5a522e06a5 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -927,8 +927,8 @@ let whd_simpl_orelse_delta_but_fix_old env sigma c =
let whd_simpl_stack =
if Flags.profile then
- let key = Profile.declare_profile "whd_simpl_stack" in
- Profile.profile3 key whd_simpl_stack
+ let key = CProfile.declare_profile "whd_simpl_stack" in
+ CProfile.profile3 key whd_simpl_stack
else whd_simpl_stack
(* Same as [whd_simpl] but also reduces constants that do not hide a
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 2e213a51d7..b49da57a4b 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -552,8 +552,8 @@ let solve_all_instances env evd filter unique split fail =
Hook.get get_solve_all_instances env evd filter unique split fail
(** Profiling resolution of typeclasses *)
-(* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *)
-(* let solve_problem = Profile.profile5 solve_classeskey solve_problem *)
+(* let solve_classeskey = CProfile.declare_profile "solve_typeclasses" *)
+(* let solve_problem = CProfile.profile5 solve_classeskey solve_problem *)
let resolve_typeclasses ?(fast_path = true) ?(filter=no_goals) ?(unique=get_typeclasses_unique_solutions ())
?(split=true) ?(fail=true) env evd =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 84ffab4260..30674fee27 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1077,13 +1077,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
in
try
let opt' = {opt with with_types = false} in
- let (substn,_,_) = Reductionops.Stack.fold2
+ let substn = Reductionops.Stack.fold2
(fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u))
(evd,ms,es) us2 us in
- let (substn,_,_) = Reductionops.Stack.fold2
+ let substn = Reductionops.Stack.fold2
(fun s u1 u -> unirec_rec curenvnb pb opt' s u1 (substl ks u))
substn params1 params in
- let (substn,_,_) = Reductionops.Stack.fold2 (fun s u1 u2 -> unirec_rec curenvnb pb opt' s u1 u2) substn ts ts1 in
+ let substn = Reductionops.Stack.fold2 (fun s u1 u2 -> unirec_rec curenvnb pb opt' s u1 u2) substn ts ts1 in
let app = mkApp (c, Array.rev_of_list ks) in
(* let substn = unirec_rec curenvnb pb b false substn t cN in *)
unirec_rec curenvnb pb opt' substn c1 app
@@ -2015,8 +2015,8 @@ let w_unify env evd cv_pb flags ty1 ty2 =
let w_unify =
if Flags.profile then
- let wunifkey = Profile.declare_profile "w_unify" in
- Profile.profile6 wunifkey w_unify
+ let wunifkey = CProfile.declare_profile "w_unify" in
+ CProfile.profile6 wunifkey w_unify
else w_unify
let w_unify env evd cv_pb ?(flags=default_unify_flags ()) ty1 ty2 =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 21:54:30 +0000