diff options
Diffstat (limited to 'pretyping/find_subterm.ml')
-rw-r--r-- | pretyping/find_subterm.ml | 34 |
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 |