aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/find_subterm.ml
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping/find_subterm.ml')
-rw-r--r--pretyping/find_subterm.ml34
1 files changed, 19 insertions, 15 deletions
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 4b9cf415f..3fc569fc4 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -11,7 +11,7 @@ open Util
open CErrors
open Names
open Locus
-open Term
+open EConstr
open Nameops
open Termops
open Pretype_errors
@@ -63,7 +63,10 @@ let proceed_with_occurrences f occs x =
let map_named_declaration_with_hyploc f hyploc acc decl =
let open Context.Named.Declaration in
- let f = f (Some (NamedDecl.get_id decl, hyploc)) in
+ let f acc typ =
+ let acc, typ = f (Some (NamedDecl.get_id decl, hyploc)) acc typ in
+ acc, typ
+ in
match decl,hyploc with
| LocalAssum (id,_), InHypValueOnly ->
error_occurrences_error (IncorrectInValueOccurrence id)
@@ -82,10 +85,10 @@ let map_named_declaration_with_hyploc f hyploc acc decl =
exception SubtermUnificationError of subterm_unification_error
-exception NotUnifiable of (constr * constr * unification_error) option
+exception NotUnifiable of (EConstr.t * EConstr.t * unification_error) option
type 'a testing_function = {
- match_fun : 'a -> constr -> 'a;
+ match_fun : 'a -> EConstr.constr -> 'a;
merge_fun : 'a -> 'a -> 'a;
mutable testing_state : 'a;
mutable last_found : position_reporting option
@@ -96,7 +99,7 @@ type 'a testing_function = {
(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 like_first test bywhat cl occ t =
+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
@@ -130,23 +133,23 @@ let replace_term_occ_gen_modulo occs like_first test bywhat cl occ 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
+ 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')
-let replace_term_occ_modulo occs test bywhat t =
+let replace_term_occ_modulo evd occs test bywhat t =
let occs',like_first =
match occs with AtOccs occs -> occs,false | LikeFirst -> AllOccurrences,true in
proceed_with_occurrences
- (replace_term_occ_gen_modulo occs' like_first test bywhat None) occs' t
+ (replace_term_occ_gen_modulo evd occs' like_first test bywhat None) occs' t
-let replace_term_occ_decl_modulo occs test bywhat d =
+let replace_term_occ_decl_modulo evd occs test bywhat d =
let (plocs,hyploc),like_first =
match occs with AtOccs occs -> occs,false | LikeFirst -> (AllOccurrences,InHyp),true in
proceed_with_occurrences
(map_named_declaration_with_hyploc
- (replace_term_occ_gen_modulo plocs like_first test bywhat)
+ (replace_term_occ_gen_modulo evd plocs like_first test bywhat)
hyploc)
plocs d
@@ -154,11 +157,12 @@ let replace_term_occ_decl_modulo occs test bywhat d =
let make_eq_univs_test env evd c =
{ match_fun = (fun evd c' ->
- let b, cst = Universes.eq_constr_universes_proj env c c' in
- if b then
+ match EConstr.eq_constr_universes_proj env evd c c' with
+ | None -> raise (NotUnifiable None)
+ | Some cst ->
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
@@ -167,7 +171,7 @@ let make_eq_univs_test env evd c =
let subst_closed_term_occ env evd occs c t =
let test = make_eq_univs_test env evd c in
let bywhat () = mkRel 1 in
- let t' = replace_term_occ_modulo occs test bywhat t in
+ let t' = replace_term_occ_modulo evd occs test bywhat t in
t', test.testing_state
let subst_closed_term_occ_decl env evd occs c d =
@@ -177,6 +181,6 @@ let subst_closed_term_occ_decl env evd occs c d =
let bywhat () = mkRel 1 in
proceed_with_occurrences
(map_named_declaration_with_hyploc
- (fun _ -> replace_term_occ_gen_modulo plocs like_first test bywhat None)
+ (fun _ -> replace_term_occ_gen_modulo evd plocs like_first test bywhat None)
hyploc) plocs d,
test.testing_state