Dead code + typo.

1 files changed, 0 insertions, 69 deletions

diff --git a/pretyping/find_subterm.ml b/pretyping/find_subterm.ml
index 2ffbee4d0..30233cdf9 100644
--- a/pretyping/find_subterm.ml
+++ b/pretyping/find_subterm.ml
@@ -92,75 +92,6 @@ 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 *)
 
-(*
-type 'a loc_state = {
-  hyp_location : (Id.t * hyp_location_flag) option;
-  maxocc : bool * int;
-  locs : occurrences;
-  current : int;
-  like_first : bool
-}
-
-let all_found pos =
-  let nowhere_except_in, maxocc = pos.maxocc in
-  nowhere_except_in && pos.current > maxocc
-
-let is_selected pos = Locusops.is_selected pos.current pos.locs
-
-let incr pos = pos := { !pos with current = (!pos).current + 1 }
-
-let make_current_pos cl pos = function
-  | AtOccs occs ->
-    let nowhere_except_in,locs = Locusops.convert_occs occs in
-    let maxocc = List.fold_right max locs 0 in
-    { hyp_location = cl;
-      maxocc = (nowhere_except_in,maxocc);
-      locs = occs;
-      current = pos;
-      like_first = false }
-  | LikeFirst ->
-    { hyp_location = None;
-      maxocc = (false,max_int);
-      locs = AllOccurrences;
-      current = pos;
-      like_first = true }
-
-let extract pos = (pos.hyp_location,pos.current)
-
-let like_first pos = pos.like_first
-
-let replace_term_occ_gen_modulo occs test bywhat cl pos t =
-  let nested = ref false in
-  let currentpos = ref (make_current_pos cl pos occs) in
-  let add_subst t subst =
-    try
-      test.testing_state <- test.merge_fun subst test.testing_state;
-      test.last_found <- Some (extract !currentpos,t)
-    with NotUnifiable e when not (like_first !currentpos) ->
-      let lastpos = Option.get test.last_found in
-     raise
-       (SubtermUnificationError (!nested,(extract !currentpos,t),lastpos,e)) in
-  let rec substrec k t =
-    if all_found !currentpos then (* shortcut *) t else
-    try
-      let subst = test.match_fun test.testing_state t in
-      if is_selected !currentpos then
-        (add_subst t subst; incr currentpos;
-         (* Check nested matching subterms *)
-         nested := true; ignore (subst_below k t); nested := false;
-         (* Do the effective substitution *)
-         Vars.lift k (bywhat ()))
-      else
-        (incr currentpos; subst_below k 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
-  in
-  let t' = substrec 0 t in
-  (!currentpos, t')
-*)
-
 let replace_term_occ_gen_modulo 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