diff options
Diffstat (limited to 'pretyping/find_subterm.ml')
| -rw-r--r-- | pretyping/find_subterm.ml | 26 |
1 files changed, 14 insertions, 12 deletions
diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml index 6733b7fc..4caa1e99 100644 --- a/pretyping/find_subterm.ml +++ b/pretyping/find_subterm.ml @@ -8,7 +8,7 @@ open Pp open Util -open Errors +open CErrors open Names open Locus open Term @@ -59,19 +59,22 @@ let proceed_with_occurrences f occs 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 -> +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 + match decl,hyploc with + | LocalAssum (id,_), 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 -> + | LocalAssum (id,typ), _ -> + let acc,typ = f acc typ in acc, LocalAssum (id,typ) + | LocalDef (id,body,typ), InHypTypeOnly -> + let acc,typ = f acc typ in acc, LocalDef (id,body,typ) + | LocalDef (id,body,typ), InHypValueOnly -> + let acc,body = f acc body in acc, LocalDef (id,body,typ) + | LocalDef (id,body,typ), InHyp -> let acc,body = f acc body in let acc,typ = f acc typ in - acc,(id,Some body,typ) + acc, LocalDef (id,body,typ) (** Finding a subterm up to some testing function *) @@ -105,7 +108,6 @@ let replace_term_occ_gen_modulo occs like_first test bywhat cl occ t = raise (SubtermUnificationError (!nested,((cl,!pos),t),lastpos,e)) in let rec substrec k t = if nowhere_except_in && !pos > maxocc then t else - if not (Vars.closed0 t) then subst_below k t else try let subst = test.match_fun test.testing_state t in if Locusops.is_selected !pos occs then |