diff options
Diffstat (limited to 'pretyping/find_subterm.ml')
| -rw-r--r-- | pretyping/find_subterm.ml | 51 |
1 files changed, 29 insertions, 22 deletions
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 4caa1e99..b1608703 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -1,9 +1,11 @@ (************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) (************************************************************************) open Pp @@ -11,11 +13,12 @@ open Util open CErrors open Names open Locus -open Term -open Nameops +open EConstr open Termops open Pretype_errors +module NamedDecl = Context.Named.Declaration + (** Processing occurrences *) type occurrence_error = @@ -28,14 +31,14 @@ let explain_invalid_occurrence l = ++ prlist_with_sep spc int l ++ str "." let explain_incorrect_in_value_occurrence id = - pr_id id ++ str " has no value." + 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 = - errorlabstrm "" (explain_occurrence_error e) + user_err (explain_occurrence_error e) let error_invalid_occurrence occ = error_occurrences_error (InvalidOccurrence occ) @@ -61,7 +64,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 (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) @@ -80,10 +86,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 @@ -94,7 +100,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 @@ -128,23 +134,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 @@ -152,11 +158,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 @@ -165,7 +172,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 = @@ -175,6 +182,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 |