From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 pretyping/find_subterm.ml | 26 ++++++++++++++------------
 1 file changed, 14 insertions(+), 12 deletions(-)

(limited to 'pretyping/find_subterm.ml')

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
-- 
cgit v1.2.3