diff options
author | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-27 21:37:56 +0200 |
---|---|---|
committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-28 18:52:55 +0200 |
commit | 1f0e44c96872196d0051618de77c4735eb447540 (patch) | |
tree | 8b69aa789ebff430d021af431ad9ad453883ba25 /pretyping | |
parent | efa921c807e48cfc19943d2bfd7f4eb11f8f9e09 (diff) |
Moved code for finding subterms (pattern, induction, set, generalize, ...)
into a specific new cleaned file find_subterm.ml.
This makes things clearer but also solves some dependencies problem
between Evd, Termops and Pretype_errors.
Diffstat (limited to 'pretyping')
-rw-r--r-- | pretyping/find_subterm.ml | 166 | ||||
-rw-r--r-- | pretyping/find_subterm.mli | 66 | ||||
-rw-r--r-- | pretyping/pretype_errors.ml | 6 | ||||
-rw-r--r-- | pretyping/pretype_errors.mli | 6 | ||||
-rw-r--r-- | pretyping/pretyping.mllib | 1 | ||||
-rw-r--r-- | pretyping/tacred.ml | 19 | ||||
-rw-r--r-- | pretyping/tacred.mli | 8 | ||||
-rw-r--r-- | pretyping/termops.ml | 136 | ||||
-rw-r--r-- | pretyping/termops.mli | 50 | ||||
-rw-r--r-- | pretyping/unification.ml | 27 |
10 files changed, 261 insertions, 224 deletions
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml new file mode 100644 index 000000000..61bb2ce03 --- /dev/null +++ b/pretyping/find_subterm.ml @@ -0,0 +1,166 @@ +(************************************************************************) +(* 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 Pp +open Util +open Errors +open Names +open Locus +open Context +open Term +open Nameops +open Termops +open Pretype_errors + +(** 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 = + pr_id 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 = + errorlabstrm "" (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 + | _ -> + (* TODO FINISH ADAPTING WITH HUGO *) + 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; + x + +(** Applying a function over a named_declaration with an hypothesis + location request *) + +let map_named_declaration_with_hyploc f hyploc acc (id,bodyopt,typ) = + let f = f (Some (id,hyploc)) in + match bodyopt,hyploc with + | None, InHypValueOnly -> + error_occurrences_error (IncorrectInValueOccurrence id) + | None, _ | Some _, InHypTypeOnly -> + let acc,typ = f acc typ in acc,(id,bodyopt,typ) + | Some body, InHypValueOnly -> + let acc,body = f acc body in acc,(id,Some body,typ) + | Some body, InHyp -> + let acc,body = f acc body in + let acc,typ = f acc typ in + acc,(id,Some body,typ) + +(** Finding a subterm up to some testing function *) + +exception SubtermUnificationError of subterm_unification_error + +exception NotUnifiable of (constr * constr * unification_error) option + +type 'a testing_function = { + match_fun : 'a -> constr -> 'a; + merge_fun : 'a -> 'a -> 'a; + mutable testing_state : 'a; + mutable last_found : ((Id.t * hyp_location_flag) option * int * constr) option +} + +(* Find subterms using a testing function, but only at a list of + locations or excluding a list of locations; in the occurrences list + (b,l), b=true means no occurrence except the ones in l and b=false, + means all occurrences except the ones in l *) + +let replace_term_occ_gen_modulo occs 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 nested = ref false in + let add_subst t subst = + try + test.testing_state <- test.merge_fun subst test.testing_state; + test.last_found <- Some (cl,!pos,t) + with NotUnifiable e -> + let lastpos = Option.get test.last_found in + raise (SubtermUnificationError (!nested,(cl,!pos,t),lastpos,e)) in + let rec substrec k t = + if nowhere_except_in && !pos > maxocc then t else + try + let subst = test.match_fun test.testing_state t in + if Locusops.is_selected !pos occs then + (add_subst t subst; incr pos; + (* Check nested matching subterms *) + nested := true; ignore (subst_below k t); nested := false; + (* Do the effective substitution *) + Vars.lift k (bywhat ())) + else + (incr pos; subst_below k t) + with NotUnifiable _ -> + subst_below k t + and subst_below k t = + map_constr_with_binders_left_to_right (fun d k -> k+1) substrec k t + in + let t' = substrec 0 t in + (!pos, t') + +let replace_term_occ_modulo occs test bywhat t = + proceed_with_occurrences + (replace_term_occ_gen_modulo occs test bywhat None) occs t + +let replace_term_occ_decl_modulo (plocs,hyploc) test bywhat d = + proceed_with_occurrences + (map_named_declaration_with_hyploc + (replace_term_occ_gen_modulo plocs test bywhat) + hyploc) + plocs d + +(** Finding an exact subterm *) + +let make_eq_univs_test evd c = + { match_fun = (fun evd c' -> + let b, cst = Universes.eq_constr_universes c c' in + if b then + try Evd.add_universe_constraints evd cst + with Evd.UniversesDiffer -> raise (NotUnifiable None) + else raise (NotUnifiable None)); + merge_fun = (fun evd _ -> evd); + testing_state = evd; + last_found = None +} + +let subst_closed_term_occ evd occs c t = + let test = make_eq_univs_test evd c in + let bywhat () = mkRel 1 in + let t' = replace_term_occ_modulo occs test bywhat t in + t', test.testing_state + +let subst_closed_term_occ_decl evd (plocs,hyploc) c d = + let test = make_eq_univs_test evd c in + let bywhat () = mkRel 1 in + proceed_with_occurrences + (map_named_declaration_with_hyploc + (fun _ -> replace_term_occ_gen_modulo plocs test bywhat None) + hyploc) plocs d, + test.testing_state diff --git a/pretyping/find_subterm.mli b/pretyping/find_subterm.mli new file mode 100644 index 000000000..44e435e69 --- /dev/null +++ b/pretyping/find_subterm.mli @@ -0,0 +1,66 @@ +(************************************************************************) +(* 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 Names +open Locus +open Context +open Term +open Evd +open Pretype_errors + +(** Finding subterms, possibly up to some unification function, + possibly at some given occurrences *) + +exception NotUnifiable of (constr * constr * unification_error) option + +exception SubtermUnificationError of subterm_unification_error + +(** A testing function is typically a unification function returning a + substitution or failing with a NotUnifiable error, together with a + function to merge substitutions and an initial substitution; + last_found is used for error messages and it has to be initialized + with None. *) +type 'a testing_function = { + match_fun : 'a -> constr -> 'a; + merge_fun : 'a -> 'a -> 'a; + mutable testing_state : 'a; + mutable last_found : ((Id.t * hyp_location_flag) option * int * constr) option +} + +(** This is the basic testing function, looking for exact matches of a + closed term *) +val make_eq_univs_test : evar_map -> constr -> evar_map testing_function + +(** [replace_term_occ_modulo occl test mk c] looks in [c] for subterm + modulo a testing function [test] and replaces successfully + matching subterms at the indicated occurrences [occl] with [mk + ()]; it turns a NotUnifiable exception raised by the testing + function into a SubtermUnificationError. *) +val replace_term_occ_modulo : + occurrences -> 'a testing_function -> (unit -> constr) -> constr -> constr + +(** [replace_term_occ_decl_modulo] is similar to + [replace_term_occ_modulo] but for a named_declaration. *) +val replace_term_occ_decl_modulo : + occurrences * hyp_location_flag -> 'a testing_function -> (unit -> constr) -> + named_declaration -> named_declaration + +(** [subst_closed_term_occ occl c d] replaces occurrences of + closed [c] at positions [occl] by [Rel 1] in [d] (see also Note OCC), + unifying universes which results in a set of constraints. *) +val subst_closed_term_occ : evar_map -> occurrences -> constr -> + constr -> constr * evar_map + +(** [subst_closed_term_occ_decl evd occl c decl] replaces occurrences of + closed [c] at positions [occl] by [Rel 1] in [decl]. *) +val subst_closed_term_occ_decl : evar_map -> + occurrences * hyp_location_flag -> + constr -> named_declaration -> named_declaration * evar_map + +(** Miscellaneous *) +val error_invalid_occurrence : int list -> 'a diff --git a/pretyping/pretype_errors.ml b/pretyping/pretype_errors.ml index d8f51054d..934e7bdbb 100644 --- a/pretyping/pretype_errors.ml +++ b/pretyping/pretype_errors.ml @@ -23,6 +23,10 @@ type unification_error = | InstanceNotSameType of existential_key * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency +type position =(Id.t * Locus.hyp_location_flag) option + +type subterm_unification_error = bool * (position * int * constr) * (position * int * constr) * (constr * constr * unification_error) option + type pretype_error = (* Old Case *) | CantFindCaseType of constr @@ -46,7 +50,7 @@ type pretype_error = | UnexpectedType of constr * constr | NotProduct of constr | TypingError of type_error - | CannotUnifyOccurrences of Termops.subterm_unification_error + | CannotUnifyOccurrences of subterm_unification_error exception PretypeError of env * Evd.evar_map * pretype_error diff --git a/pretyping/pretype_errors.mli b/pretyping/pretype_errors.mli index f8e39f316..e816463e7 100644 --- a/pretyping/pretype_errors.mli +++ b/pretyping/pretype_errors.mli @@ -24,6 +24,10 @@ type unification_error = | InstanceNotSameType of existential_key * env * types * types | UnifUnivInconsistency of Univ.univ_inconsistency +type position =(Id.t * Locus.hyp_location_flag) option + +type subterm_unification_error = bool * (position * int * constr) * (position * int * constr) * (constr * constr * unification_error) option + type pretype_error = (** Old Case *) | CantFindCaseType of constr @@ -47,7 +51,7 @@ type pretype_error = | UnexpectedType of constr * constr | NotProduct of constr | TypingError of type_error - | CannotUnifyOccurrences of Termops.subterm_unification_error + | CannotUnifyOccurrences of subterm_unification_error exception PretypeError of env * Evd.evar_map * pretype_error diff --git a/pretyping/pretyping.mllib b/pretyping/pretyping.mllib index f1a9d6915..ceb01fd95 100644 --- a/pretyping/pretyping.mllib +++ b/pretyping/pretyping.mllib @@ -9,6 +9,7 @@ Nativenorm Retyping Cbv Pretype_errors +Find_subterm Evarutil Evarsolve Recordops diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 75f6f66fe..6e522933f 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -15,6 +15,7 @@ open Vars open Libnames open Globnames open Termops +open Find_subterm open Namegen open Environ open Closure @@ -1075,22 +1076,6 @@ let compute = cbv_betadeltaiota (* Pattern *) -let make_eq_univs_test evd c = - { match_fun = (fun evd c' -> - let b, cst = Universes.eq_constr_universes c c' in - if b then - try Evd.add_universe_constraints evd cst - with Evd.UniversesDiffer -> raise NotUnifiable - else raise NotUnifiable); - merge_fun = (fun evd _ -> evd); - testing_state = evd; - last_found = None -} -let subst_closed_term_univs_occ evd occs c t = - let test = make_eq_univs_test evd c in - let t' = subst_closed_term_occ_modulo occs test None t in - t', test.testing_state - (* gives [na:ta]c' such that c converts to ([na:ta]c' a), abstracting only * the specified occurrences. *) @@ -1101,7 +1086,7 @@ let abstract_scheme env sigma (locc,a) c = if occur_meta a then mkLambda (na,ta,c) else - let c', sigma' = subst_closed_term_univs_occ sigma locc a c in + let c', sigma' = subst_closed_term_occ sigma locc a c in mkLambda (na,ta,c') let pattern_occs loccs_trm env sigma c = diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli index 5e4bc5c46..91364c4ae 100644 --- a/pretyping/tacred.mli +++ b/pretyping/tacred.mli @@ -60,14 +60,6 @@ val unfoldn : (** Fold *) val fold_commands : constr list -> reduction_function -val make_eq_univs_test : evar_map -> constr -> evar_map Termops.testing_function - -(** [subst_closed_term_occ occl c d] replaces occurrences of closed [c] at - positions [occl] by [Rel 1] in [d] (see also Note OCC), unifying universes - which results in a set of constraints. *) -val subst_closed_term_univs_occ : evar_map -> occurrences -> constr -> constr -> - constr * evar_map - (** Pattern *) val pattern_occs : (occurrences * constr) list -> env -> evar_map -> constr -> constr diff --git a/pretyping/termops.ml b/pretyping/termops.ml index c68f2c4d9..67ffcf8aa 100644 --- a/pretyping/termops.ml +++ b/pretyping/termops.ml @@ -679,142 +679,6 @@ let replace_term_gen eq_fun c by_c in_t = let replace_term = replace_term_gen eq_constr -(* Substitute only at a list of locations or excluding a list of - locations; in the occurrences list (b,l), b=true means no - occurrence except the ones in l and b=false, means all occurrences - except the ones in l *) - -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 = - pr_id 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 = - errorlabstrm "" (explain_occurrence_error e) - -let error_invalid_occurrence occ = - error_occurrences_error (InvalidOccurrence occ) - -type position =(Id.t * Locus.hyp_location_flag) option - -type subterm_unification_error = bool * (position * int * constr) * (position * int * constr) - -exception SubtermUnificationError of subterm_unification_error - -exception NotUnifiable - -type 'a testing_function = { - match_fun : 'a -> constr -> 'a; - merge_fun : 'a -> 'a -> 'a; - mutable testing_state : 'a; - mutable last_found : ((Id.t * hyp_location_flag) option * int * constr) option -} - -let subst_closed_term_occ_gen_modulo occs test 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 nested = ref false in - let add_subst t subst = - try - test.testing_state <- test.merge_fun subst test.testing_state; - test.last_found <- Some (cl,!pos,t) - with NotUnifiable -> - let lastpos = Option.get test.last_found in - raise (SubtermUnificationError (!nested,(cl,!pos,t),lastpos)) in - let rec substrec k t = - if nowhere_except_in && !pos > maxocc then t else - try - let subst = test.match_fun test.testing_state t in - if Locusops.is_selected !pos occs then - (add_subst t subst; incr pos; - (* Check nested matching subterms *) - nested := true; ignore (subst_below k t); nested := false; - (* Do the effective substitution *) - mkRel k) - else - (incr pos; subst_below k t) - with NotUnifiable -> - subst_below k t - and subst_below k t = - map_constr_with_binders_left_to_right (fun d k -> k+1) substrec k t - in - let t' = substrec 1 t in - (!pos, t') - -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 - | _ -> - (* TODO FINISH ADAPTING WITH HUGO *) - 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; - x - -let make_eq_test c = { - match_fun = (fun () c' -> if eq_constr c c' then () else raise NotUnifiable); - merge_fun = (fun () () -> ()); - testing_state = (); - last_found = None -} - -let subst_closed_term_occ_gen occs pos c t = - subst_closed_term_occ_gen_modulo occs (make_eq_test c) None pos t - -let subst_closed_term_occ occs c t = - proceed_with_occurrences - (fun occ -> subst_closed_term_occ_gen occs occ c) - occs t - -let subst_closed_term_occ_modulo occs test cl t = - proceed_with_occurrences - (subst_closed_term_occ_gen_modulo occs test cl) occs t - -let map_named_declaration_with_hyploc f hyploc acc (id,bodyopt,typ) = - let f = f (Some (id,hyploc)) in - match bodyopt,hyploc with - | None, InHypValueOnly -> - error_occurrences_error (IncorrectInValueOccurrence id) - | None, _ | Some _, InHypTypeOnly -> - let acc,typ = f acc typ in acc,(id,bodyopt,typ) - | Some body, InHypValueOnly -> - let acc,body = f acc body in acc,(id,Some body,typ) - | Some body, InHyp -> - let acc,body = f acc body in - let acc,typ = f acc typ in - acc,(id,Some body,typ) - -let subst_closed_term_occ_decl (plocs,hyploc) c d = - proceed_with_occurrences - (map_named_declaration_with_hyploc - (fun _ occ -> subst_closed_term_occ_gen plocs occ c) hyploc) plocs d - -let subst_closed_term_occ_decl_modulo (plocs,hyploc) test d = - proceed_with_occurrences - (map_named_declaration_with_hyploc - (subst_closed_term_occ_gen_modulo plocs test) - hyploc) - plocs d - let vars_of_env env = let s = Context.fold_named_context (fun (id,_,_) s -> Id.Set.add id s) diff --git a/pretyping/termops.mli b/pretyping/termops.mli index ebcf4285c..e01b3f455 100644 --- a/pretyping/termops.mli +++ b/pretyping/termops.mli @@ -147,56 +147,6 @@ val subst_term : constr -> constr -> constr (** [replace_term d e c] replaces [d] by [e] in [c] *) val replace_term : constr -> constr -> constr -> constr -(** [subst_closed_term_occ_gen occl n c d] replaces occurrences of closed [c] at - positions [occl], counting from [n], by [Rel 1] in [d] *) -val subst_closed_term_occ_gen : - occurrences -> int -> constr -> types -> int * types - -(** [subst_closed_term_occ_modulo] looks for subterm modulo a - testing function returning a substitution of type ['a] (or failing - with NotUnifiable); a function for merging substitution (possibly - failing with NotUnifiable) and an initial substitution are - required too; [subst_closed_term_occ_modulo] itself turns a - NotUnifiable exception into a SubtermUnificationError *) - -exception NotUnifiable - -type position =(Id.t * Locus.hyp_location_flag) option - -type subterm_unification_error = bool * (position * int * constr) * (position * int * constr) - -exception SubtermUnificationError of subterm_unification_error - -type 'a testing_function = { - match_fun : 'a -> constr -> 'a; - merge_fun : 'a -> 'a -> 'a; - mutable testing_state : 'a; - mutable last_found : ((Id.t * hyp_location_flag) option * int * constr) option -} - -val make_eq_test : constr -> unit testing_function - -val subst_closed_term_occ_modulo : - occurrences -> 'a testing_function -> (Id.t * hyp_location_flag) option - -> constr -> types - -(** [subst_closed_term_occ occl c d] replaces occurrences of closed [c] at - positions [occl] by [Rel 1] in [d] (see also Note OCC) *) -val subst_closed_term_occ : occurrences -> constr -> constr -> constr - -(** [subst_closed_term_occ_decl occl c decl] replaces occurrences of closed [c] - at positions [occl] by [Rel 1] in [decl] *) - -val subst_closed_term_occ_decl : - occurrences * hyp_location_flag -> constr -> named_declaration -> - named_declaration - -val subst_closed_term_occ_decl_modulo : - occurrences * hyp_location_flag -> 'a testing_function -> - named_declaration -> named_declaration - -val error_invalid_occurrence : int list -> 'a - (** Alternative term equalities *) val base_sort_cmp : Reduction.conv_pb -> sorts -> sorts -> bool val compare_constr_univ : (Reduction.conv_pb -> constr -> constr -> bool) -> diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 9baabae77..dd0f68390 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -26,6 +26,7 @@ open Coercion open Recordops open Locus open Locusops +open Find_subterm let occur_meta_or_undefined_evar evd c = let rec occrec c = match kind_of_term c with @@ -62,7 +63,7 @@ let abstract_scheme env evd c l lname_typ = else *) if occur_meta a then mkLambda_name env (na,ta,t), evd else - let t', evd' = Tacred.subst_closed_term_univs_occ evd locc a t in + let t', evd' = Find_subterm.subst_closed_term_occ evd locc a t in mkLambda_name env (na,ta,t'), evd') (c,evd) (List.rev l) @@ -1222,17 +1223,21 @@ let make_pattern_test inf_flags env sigma0 (sigma,c) = let matching_fun _ t = try let sigma = w_typed_unify env sigma Reduction.CONV flags c t in Some(sigma, t) - with e when Errors.noncritical e -> raise NotUnifiable in + with + | PretypeError (_,_,CannotUnify (c1,c2,Some e)) -> + raise (NotUnifiable (Some (c1,c2,e))) + | e when Errors.noncritical e -> raise (NotUnifiable None) in let merge_fun c1 c2 = match c1, c2 with | Some (evd,c1), Some (_,c2) -> (try let evd = w_typed_unify env evd Reduction.CONV flags c1 c2 in Some (evd, c1) - with e when Errors.noncritical e -> raise NotUnifiable) + with + | PretypeError (_,_,CannotUnify (c1,c2,Some e)) -> raise (NotUnifiable (Some (c1,c2,e))) + | e when Errors.noncritical e -> raise (NotUnifiable None)) | Some _, None -> c1 | None, Some _ -> c2 - | None, None -> None - in + | None, None -> None in { match_fun = matching_fun; merge_fun = merge_fun; testing_state = None; last_found = None }, (fun test -> match test.testing_state with @@ -1247,7 +1252,7 @@ let make_eq_test evd c = let out cstr = Evd.evar_universe_context cstr.testing_state, c in - (Tacred.make_eq_univs_test evd c, out) + (make_eq_univs_test evd c, out) let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env concl = let id = @@ -1260,6 +1265,7 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc else x in + let mkvarid () = mkVar id in let compute_dependency _ (hyp,_,_ as d) depdecls = match occurrences_of_hyp hyp occs with | None -> @@ -1272,7 +1278,7 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc else depdecls | Some ((AllOccurrences, InHyp) as occ) -> - let newdecl = subst_closed_term_occ_decl_modulo occ test d in + let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in if Context.eq_named_declaration d newdecl && not (indirectly_dependent c d depdecls) then @@ -1280,16 +1286,15 @@ let make_abstraction_core name (test,out) (sigmac,c) ty occs check_occs env conc then raise (PretypeError (env,sigmac,NoOccurrenceFound (c,Some hyp))) else depdecls else - (subst1_named_decl (mkVar id) newdecl)::depdecls + newdecl :: depdecls | Some occ -> - let newdecl = subst_closed_term_occ_decl_modulo occ test d in - (subst1_named_decl (mkVar id) newdecl)::depdecls in + replace_term_occ_decl_modulo occ test mkvarid d :: depdecls in try let depdecls = fold_named_context compute_dependency env ~init:[] in let ccl = match occurrences_of_goal occs with | None -> concl | Some occ -> - subst1 (mkVar id) (subst_closed_term_occ_modulo occ test None concl) + replace_term_occ_modulo occ test mkvarid concl in let lastlhyp = if List.is_empty depdecls then None else Some (pi1(List.last depdecls)) in |