aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/constr_matching.ml7
-rw-r--r--pretyping/find_subterm.ml59
-rw-r--r--pretyping/find_subterm.mli3
-rw-r--r--pretyping/locusops.ml44
-rw-r--r--pretyping/locusops.mli35
-rw-r--r--pretyping/recordops.ml19
-rw-r--r--pretyping/recordops.mli2
-rw-r--r--pretyping/reductionops.ml8
-rw-r--r--pretyping/reductionops.mli35
-rw-r--r--pretyping/tacred.ml59
-rw-r--r--pretyping/unification.ml16
11 files changed, 143 insertions, 144 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index a3f1c0b004..0e69b814c7 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -528,10 +528,9 @@ let sub_match ?(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') ->
- begin try
- let term = Retyping.expand_projection env sigma p c' [] in
- aux env term mk_ctx next
- with Retyping.RetypeError _ -> next ()
+ begin match Retyping.expand_projection env sigma p c' [] with
+ | term -> aux env term mk_ctx next
+ | exception Retyping.RetypeError _ -> next ()
end
| Array(u, t, def, ty) ->
let next_mk_ctx = function
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index bd717e2d1f..52e3364109 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -21,42 +21,15 @@ module NamedDecl = Context.Named.Declaration
(** Processing occurrences *)
-type occurrence_error =
- | InvalidOccurrence of int list
- | IncorrectInValueOccurrence of Id.t
-
-let explain_invalid_occurrence l =
- let l = List.sort_uniquize Int.compare l in
- str ("Invalid occurrence " ^ String.plural (List.length l) "number" ^": ")
- ++ prlist_with_sep spc int l ++ str "."
-
let explain_incorrect_in_value_occurrence id =
Id.print id ++ str " has no value."
-let explain_occurrence_error = function
- | InvalidOccurrence l -> explain_invalid_occurrence l
- | IncorrectInValueOccurrence id -> explain_incorrect_in_value_occurrence id
-
-let error_occurrences_error e =
- user_err (explain_occurrence_error e)
-
-let error_invalid_occurrence occ =
- error_occurrences_error (InvalidOccurrence occ)
-
-let check_used_occurrences nbocc (nowhere_except_in,locs) =
- let rest = List.filter (fun o -> o >= nbocc) locs in
- match rest with
- | [] -> ()
- | _ -> error_occurrences_error (InvalidOccurrence rest)
-
let proceed_with_occurrences f occs x =
match occs with
| NoOccurrences -> x
| occs ->
- let plocs = Locusops.convert_occs occs in
- assert (List.for_all (fun x -> x >= 0) (snd plocs));
- let (nbocc,x) = f 1 x in
- check_used_occurrences nbocc plocs;
+ let (occs,x) = f (Locusops.initialize_occurrence_counter occs) x in
+ Locusops.check_used_occurrences occs;
x
(** Applying a function over a named_declaration with an hypothesis
@@ -70,7 +43,7 @@ let map_named_declaration_with_hyploc f hyploc acc decl =
in
match decl,hyploc with
| LocalAssum (id,_), InHypValueOnly ->
- error_occurrences_error (IncorrectInValueOccurrence id.Context.binder_name)
+ user_err (explain_incorrect_in_value_occurrence id.Context.binder_name)
| LocalAssum (id,typ), _ ->
let acc,typ = f acc typ in acc, LocalAssum (id,typ)
| LocalDef (id,body,typ), InHypTypeOnly ->
@@ -101,43 +74,43 @@ type 'a testing_function = {
means all occurrences except the ones in l *)
let replace_term_occ_gen_modulo sigma occs like_first test bywhat cl occ t =
- let (nowhere_except_in,locs) = Locusops.convert_occs occs in
- let maxocc = List.fold_right max locs 0 in
- let pos = ref occ in
+ let count = ref (Locusops.initialize_occurrence_counter occs) in
let nested = ref false in
- let add_subst t subst =
+ let add_subst pos t subst =
try
test.testing_state <- test.merge_fun subst test.testing_state;
- test.last_found <- Some ((cl,!pos),t)
+ test.last_found <- Some ((cl,pos),t)
with NotUnifiable e when not like_first ->
let lastpos = Option.get test.last_found in
- raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,e)) in
+ raise (SubtermUnificationError (!nested,((cl,pos),t),lastpos,e)) in
let rec substrec k t =
- if nowhere_except_in && !pos > maxocc then t else
+ if Locusops.occurrences_done !count then t else
try
let subst = test.match_fun test.testing_state t in
- if Locusops.is_selected !pos occs then
+ let selected, count' = Locusops.update_occurrence_counter !count in count := count';
+ if selected then
+ let pos = Locusops.current_occurrence !count in
(if !nested then begin
(* in case it is nested but not later detected as unconvertible,
as when matching "id _" in "id (id 0)" *)
let lastpos = Option.get test.last_found in
- raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,None))
+ raise (SubtermUnificationError (!nested,((cl,pos),t),lastpos,None))
end;
- add_subst t subst; incr pos;
+ add_subst pos t subst;
(* Check nested matching subterms *)
- if not (Locusops.is_all_occurrences occs) && occs != Locus.NoOccurrences then
+ if Locusops.more_specific_occurrences !count then
begin nested := true; ignore (subst_below k t); nested := false end;
(* Do the effective substitution *)
Vars.lift k (bywhat ()))
else
- (incr pos; subst_below k t)
+ subst_below k t
with NotUnifiable _ ->
subst_below k t
and subst_below k t =
map_constr_with_binders_left_to_right sigma (fun d k -> k+1) substrec k t
in
let t' = substrec 0 t in
- (!pos, t')
+ (!count, t')
let replace_term_occ_modulo evd occs test bywhat t =
let occs',like_first =
diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli
index 436b730a88..1ddae01e2b 100644
--- a/pretyping/find_subterm.mli
+++ b/pretyping/find_subterm.mli
@@ -65,6 +65,3 @@ val subst_closed_term_occ : env -> evar_map -> occurrences or_like_first ->
val subst_closed_term_occ_decl : env -> evar_map ->
(occurrences * hyp_location_flag) or_like_first ->
constr -> named_declaration -> named_declaration * evar_map
-
-(** Miscellaneous *)
-val error_invalid_occurrence : int list -> 'a
diff --git a/pretyping/locusops.ml b/pretyping/locusops.ml
index 86352eb79a..256d61a32b 100644
--- a/pretyping/locusops.ml
+++ b/pretyping/locusops.ml
@@ -8,6 +8,7 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
+open Util
open Locus
(** Utilities on or_var *)
@@ -27,12 +28,43 @@ let occurrences_map f = function
if l' = [] then AllOccurrences else AllOccurrencesBut l'
| (NoOccurrences|AllOccurrences|AtLeastOneOccurrence) as o -> o
-let convert_occs = function
- | AtLeastOneOccurrence -> (false,[])
- | AllOccurrences -> (false,[])
- | AllOccurrencesBut l -> (false,l)
- | NoOccurrences -> (true,[])
- | OnlyOccurrences l -> (true,l)
+type occurrences_count = {current: int; remaining: int list; where: (bool * int)}
+
+let error_invalid_occurrence l =
+ CErrors.user_err Pp.(str ("Invalid occurrence " ^ String.plural (List.length l) "number" ^": ")
+ ++ prlist_with_sep spc int l ++ str ".")
+
+let initialize_occurrence_counter occs =
+ let (nowhere_except_in,occs) =
+ match occs with
+ | AtLeastOneOccurrence -> (false,[])
+ | AllOccurrences -> (false,[])
+ | AllOccurrencesBut l -> (false,List.sort_uniquize Int.compare l)
+ | NoOccurrences -> (true,[])
+ | OnlyOccurrences l -> (true,List.sort_uniquize Int.compare l) in
+ let max =
+ match occs with
+ | n::_ when n <= 0 -> error_invalid_occurrence [n]
+ | [] -> 0
+ | _ -> Util.List.last occs in
+ {current = 0; remaining = occs; where = (nowhere_except_in,max)}
+
+let update_occurrence_counter {current; remaining; where = (nowhere_except_in,_ as where)} =
+ let current = succ current in
+ match remaining with
+ | occ::remaining when Int.equal current occ -> (nowhere_except_in,{current;remaining;where})
+ | _ -> (not nowhere_except_in,{current;remaining;where})
+
+let check_used_occurrences {remaining} =
+ if not (Util.List.is_empty remaining) then error_invalid_occurrence remaining
+
+let occurrences_done {current; where = (nowhere_except_in,max)} =
+ nowhere_except_in && current > max
+
+let current_occurrence {current} = current
+
+let more_specific_occurrences {current; where = (_,max)} =
+ current <= max
let is_selected occ = function
| AtLeastOneOccurrence -> true
diff --git a/pretyping/locusops.mli b/pretyping/locusops.mli
index 911ccc1a38..748bfbc252 100644
--- a/pretyping/locusops.mli
+++ b/pretyping/locusops.mli
@@ -20,13 +20,44 @@ val or_var_map : ('a -> 'b) -> 'a or_var -> 'b or_var
val occurrences_map :
('a list -> 'b list) -> 'a occurrences_gen -> 'b occurrences_gen
-(** From occurrences to a list of positions (or complement of positions) *)
-val convert_occs : occurrences -> bool * int list
+(** {6 Counting occurrences} *)
+
+type occurrences_count
+ (** A counter of occurrences associated to a list of occurrences *)
+
+(** Three basic functions to initialize, count, and conclude a loop
+ browsing over subterms *)
+
+val initialize_occurrence_counter : occurrences -> occurrences_count
+ (** Initialize an occurrence_counter *)
+
+val update_occurrence_counter : occurrences_count -> bool * occurrences_count
+ (** Increase the occurrence counter by one and tell if the current occurrence is selected *)
+
+val check_used_occurrences : occurrences_count -> unit
+ (** Increase the occurrence counter and tell if the current occurrence is selected *)
+
+(** Auxiliary functions about occurrence counters *)
+
+val current_occurrence : occurrences_count -> int
+ (** Tell the value of the current occurrence *)
+
+val occurrences_done : occurrences_count -> bool
+ (** Tell if there are no more occurrences to select and if the loop
+ can be shortcut *)
+
+val more_specific_occurrences : occurrences_count -> bool
+ (** Tell if there are no more occurrences to select (or unselect)
+ and if an inner loop can be shortcut *)
+
+(** {6 Miscellaneous} *)
val is_selected : int -> occurrences -> bool
val is_all_occurrences : 'a occurrences_gen -> bool
+val error_invalid_occurrence : int list -> 'a
+
(** Usual clauses *)
val allHypsAndConcl : 'a clause_expr
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index b6e44265ae..aa862a912e 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -323,23 +323,32 @@ let check_and_decompose_canonical_structure env sigma ref =
let lookup_canonical_conversion env (proj,pat) =
assoc_pat env pat (GlobRef.Map.find proj !object_table)
-let decompose_projection sigma c args =
+let rec get_nth n = function
+| [] -> raise Not_found
+| arg :: args ->
+ let len = Array.length arg in
+ if n < len then arg.(n)
+ else get_nth (n - len) args
+
+let rec decompose_projection sigma c args =
match EConstr.kind sigma c with
+ | Meta mv -> decompose_projection sigma (Evd.meta_value sigma mv) args
+ | Cast (c, _, _) -> decompose_projection sigma c args
+ | App (c, arg) -> decompose_projection sigma c (arg :: args)
| Const (c, u) ->
let n = find_projection_nparams (GlobRef.ConstRef c) in
(* Check if there is some canonical projection attached to this structure *)
let _ = GlobRef.Map.find (GlobRef.ConstRef c) !object_table in
- let arg = Stack.nth args n in
- arg
+ get_nth n args
| Proj (p, c) ->
let _ = GlobRef.Map.find (GlobRef.ConstRef (Projection.constant p)) !object_table in
c
| _ -> raise Not_found
-let is_open_canonical_projection env sigma (c,args) =
+let is_open_canonical_projection env sigma c =
let open EConstr in
try
- let arg = decompose_projection sigma c args in
+ let arg = decompose_projection sigma c [] in
try
let arg = whd_all env sigma arg in
let hd = match EConstr.kind sigma arg with App (hd, _) -> hd | _ -> arg in
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 5b8dc8184a..83927085e9 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -94,7 +94,7 @@ val register_canonical_structure : warn:bool -> Environ.env -> Evd.evar_map ->
cs -> unit
val subst_canonical_structure : Mod_subst.substitution -> cs -> cs
val is_open_canonical_projection :
- Environ.env -> Evd.evar_map -> Reductionops.state -> bool
+ Environ.env -> Evd.evar_map -> EConstr.t -> bool
val canonical_projections : unit ->
((GlobRef.t * cs_pattern) * obj_typ) list
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index ac6bb52a2f..9580825010 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -930,14 +930,6 @@ let stack_red_of_state_red f =
let f env sigma x = EConstr.decompose_app sigma (Stack.zip sigma (f env sigma (x, Stack.empty))) in
f
-(* Drops the Cst_stack *)
-let iterate_whd_gen flags env sigma s =
- let rec aux t =
- let (hd,sk) = whd_state_gen flags env sigma (t,Stack.empty) in
- let whd_sk = Stack.map aux sk in
- Stack.zip sigma (hd,whd_sk)
- in aux s
-
let red_of_state_red f env sigma x =
Stack.zip sigma (f env sigma (x,Stack.empty))
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index b5471eff34..0b7f43f469 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -106,8 +106,6 @@ end
(************************************************************************)
-type state = constr * constr Stack.t
-
type reduction_function = env -> evar_map -> constr -> constr
type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
@@ -115,11 +113,6 @@ type e_reduction_function = env -> evar_map -> constr -> evar_map * constr
type stack_reduction_function =
env -> evar_map -> constr -> constr * constr list
-type state_reduction_function =
- env -> evar_map -> state -> state
-
-val pr_state : env -> evar_map -> state -> Pp.t
-
(** {6 Reduction Function Operators } *)
val strong_with_flags :
@@ -127,12 +120,6 @@ val strong_with_flags :
(CClosure.RedFlags.reds -> reduction_function)
val strong : reduction_function -> reduction_function
-val whd_state_gen :
- CClosure.RedFlags.reds -> Environ.env -> Evd.evar_map -> state -> state
-
-val iterate_whd_gen : CClosure.RedFlags.reds ->
- Environ.env -> Evd.evar_map -> constr -> constr
-
(** {6 Generic Optimized Reduction Function using Closures } *)
val clos_norm_flags : CClosure.RedFlags.reds -> reduction_function
@@ -166,24 +153,13 @@ val whd_all_stack : stack_reduction_function
val whd_allnolet_stack : stack_reduction_function
val whd_betalet_stack : stack_reduction_function
-val whd_nored_state : state_reduction_function
-val whd_beta_state : state_reduction_function
-val whd_betaiota_state : state_reduction_function
-val whd_betaiotazeta_state : state_reduction_function
-val whd_all_state : state_reduction_function
-val whd_allnolet_state : state_reduction_function
-val whd_betalet_state : state_reduction_function
-
(** {6 Head normal forms } *)
val whd_delta_stack : stack_reduction_function
-val whd_delta_state : state_reduction_function
val whd_delta : reduction_function
val whd_betadeltazeta_stack : stack_reduction_function
-val whd_betadeltazeta_state : state_reduction_function
val whd_betadeltazeta : reduction_function
val whd_zeta_stack : stack_reduction_function
-val whd_zeta_state : state_reduction_function
val whd_zeta : reduction_function
val shrink_eta : Environ.env -> constr -> constr
@@ -269,8 +245,17 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TransparentState.t ->
(** {6 Heuristic for Conversion with Evar } *)
+type state = constr * constr Stack.t
+
+type state_reduction_function =
+ env -> evar_map -> state -> state
+
+val pr_state : env -> evar_map -> state -> Pp.t
+
+val whd_nored_state : state_reduction_function
+
val whd_betaiota_deltazeta_for_iota_state :
- TransparentState.t -> Environ.env -> Evd.evar_map -> state -> state
+ TransparentState.t -> state_reduction_function
(** {6 Meta-related reduction functions } *)
type meta_instance_subst
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 9cf7119709..c705ac16e7 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1046,28 +1046,23 @@ let change_map_constr_with_binders_left_to_right g f (env, l as acc) sigma c =
| _ -> map_constr_with_binders_left_to_right sigma g f acc c
let e_contextually byhead (occs,c) f = begin fun env sigma t ->
- let (nowhere_except_in,locs) = Locusops.convert_occs occs in
- let maxocc = List.fold_right max locs 0 in
- let pos = ref 1 in
+ let count = ref (Locusops.initialize_occurrence_counter occs) in
(* FIXME: we do suspicious things with this evarmap *)
let evd = ref sigma in
let rec traverse nested (env,c as envc) t =
- if nowhere_except_in && (!pos > maxocc) then (* Shortcut *) t
+ if Locusops.occurrences_done !count then (* Shortcut *) t
else
try
let subst =
if byhead then matches_head env sigma c t
else Constr_matching.matches env sigma c t in
- let ok =
- if nowhere_except_in then Int.List.mem !pos locs
- else not (Int.List.mem !pos locs) in
- incr pos;
+ let ok, count' = Locusops.update_occurrence_counter !count in count := count';
if ok then begin
if Option.has_some nested then
- user_err (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (!pos-1) ++ str ".");
+ user_err (str "The subterm at occurrence " ++ int (Option.get nested) ++ str " overlaps with the subterm at occurrence " ++ int (Locusops.current_occurrence !count) ++ str ".");
(* Skip inner occurrences for stable counting of occurrences *)
- if locs != [] then
- ignore (traverse_below (Some (!pos-1)) envc t);
+ if Locusops.more_specific_occurrences !count then
+ ignore (traverse_below (Some (Locusops.current_occurrence !count)) envc t);
let (evm, t) = (f subst) env !evd t in
(evd := evm; t)
end
@@ -1087,7 +1082,7 @@ let e_contextually byhead (occs,c) f = begin fun env sigma t ->
(traverse nested) envc sigma t
in
let t' = traverse None (env,c) t in
- if List.exists (fun o -> o >= !pos) locs then error_invalid_occurrence locs;
+ Locusops.check_used_occurrences !count;
(!evd, t')
end
@@ -1105,28 +1100,25 @@ let match_constr_evaluable_ref sigma c evref =
| Var id, EvalVarRef id' when Id.equal id id' -> Some EInstance.empty
| _, _ -> None
-let substlin env sigma evalref n (nowhere_except_in,locs) c =
- let maxocc = List.fold_right max locs 0 in
- let pos = ref n in
- assert (List.for_all (fun x -> x >= 0) locs);
+let substlin env sigma evalref occs c =
+ let count = ref (Locusops.initialize_occurrence_counter occs) in
let value u = value_of_evaluable_ref env evalref u in
let rec substrec () c =
- if nowhere_except_in && !pos > maxocc then c
+ if Locusops.occurrences_done !count then c
else
match match_constr_evaluable_ref sigma c evalref with
| Some u ->
- let ok =
- if nowhere_except_in then Int.List.mem !pos locs
- else not (Int.List.mem !pos locs) in
- incr pos;
- if ok then value u else c
+ let ok, count' = Locusops.update_occurrence_counter !count in
+ count := count';
+ if ok then value u else c
| None ->
map_constr_with_binders_left_to_right sigma
(fun _ () -> ())
substrec () c
in
let t' = substrec () c in
- (!pos, t')
+ Locusops.check_used_occurrences !count;
+ (Locusops.current_occurrence !count, t')
let string_of_evaluable_ref env = function
| EvalVarRef id -> Id.to_string id
@@ -1154,23 +1146,14 @@ let unfold env sigma name c =
* at the occurrences of occ_list. If occ_list is empty, unfold all occurrences.
* Performs a betaiota reduction after unfolding. *)
let unfoldoccs env sigma (occs,name) c =
- let unfo nowhere_except_in locs =
- let (nbocc,uc) = substlin env sigma name 1 (nowhere_except_in,locs) c in
- if Int.equal nbocc 1 then
+ match occs with
+ | NoOccurrences -> c
+ | AllOccurrences -> unfold env sigma name c
+ | OnlyOccurrences _ | AllOccurrencesBut _ | AtLeastOneOccurrence ->
+ let (occ,uc) = substlin env sigma name occs c in
+ if Int.equal occ 0 then
user_err Pp.(str ((string_of_evaluable_ref env name)^" does not occur."));
- let rest = List.filter (fun o -> o >= nbocc) locs in
- let () = match rest with
- | [] -> ()
- | _ -> error_invalid_occurrence rest
- in
nf_betaiotazeta env sigma uc
- in
- match occs with
- | NoOccurrences -> c
- | AllOccurrences -> unfold env sigma name c
- | OnlyOccurrences l -> unfo true l
- | AllOccurrencesBut l -> unfo false l
- | AtLeastOneOccurrence -> unfo false []
(* Unfold reduction tactic: *)
let unfoldn loccname env sigma c =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 1c24578a1c..3d3010d1a4 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1070,10 +1070,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
and canonical_projections (curenv, _ as curenvnb) pb opt cM cN (sigma,_,_ as substn) =
let f1 () =
if isApp_or_Proj sigma cM then
- let f1l1 = whd_nored_state curenv sigma (cM,Stack.empty) in
- if is_open_canonical_projection curenv sigma f1l1 then
- let f2l2 = whd_nored_state curenv sigma (cN,Stack.empty) in
- solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 substn
+ if is_open_canonical_projection curenv sigma cM then
+ solve_canonical_projection curenvnb pb opt cM cN substn
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
in
@@ -1086,14 +1084,14 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
else
try f1 () with e when precatchable_exception e ->
if isApp_or_Proj sigma cN then
- let f2l2 = whd_nored_state curenv sigma (cN, Stack.empty) in
- if is_open_canonical_projection curenv sigma f2l2 then
- let f1l1 = whd_nored_state curenv sigma (cM, Stack.empty) in
- solve_canonical_projection curenvnb pb opt cN f2l2 cM f1l1 substn
+ if is_open_canonical_projection curenv sigma cN then
+ solve_canonical_projection curenvnb pb opt cN cM substn
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
else error_cannot_unify (fst curenvnb) sigma (cM,cN)
- and solve_canonical_projection curenvnb pb opt cM f1l1 cN f2l2 (sigma,ms,es) =
+ and solve_canonical_projection curenvnb pb opt cM cN (sigma,ms,es) =
+ let f1l1 = whd_nored_state (fst curenvnb) sigma (cM,Stack.empty) in
+ let f2l2 = whd_nored_state (fst curenvnb) sigma (cN,Stack.empty) in
let (ctx,t,c,bs,(params,params1),(us,us2),(ts,ts1),c1,(n,t2)) =
try Evarconv.check_conv_record (fst curenvnb) sigma f1l1 f2l2
with Not_found -> error_cannot_unify (fst curenvnb) sigma (cM,cN)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 09:36:34 +0000