Dead code + typo.

3 files changed, 1 insertions, 94 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
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 2f1c230b7..65d08609f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1418,7 +1418,7 @@ let make_pattern_test from_prefix_of_ind env sigma (pending,c) =
       let t' =
         if from_prefix_of_ind then
           (* We check for fully applied subterms of the form "u u1 .. un" *)
-          (* of inductive type knowning only a prefix "u u1 .. ui" *)
+          (* of inductive type knowing only a prefix "u u1 .. ui" *)
           let t,l = decompose_app t in
           let l1,l2 =
             try List.chop n l with Failure _ -> raise (NotUnifiable None) in
@@ -1450,10 +1450,6 @@ let make_pattern_test from_prefix_of_ind env sigma (pending,c) =
     testing_state = None; last_found = None },
   (fun test -> match test.testing_state with
   | None -> None
-(*
-     let sigma, c = finish_evar_resolution ~flags:inf_flags env sigma (pending,c) in
-     sigma,c
-*)
   | Some (sigma,_) ->
      let c = nf_evar sigma (local_strong whd_meta sigma c) in
      let univs, subst = nf_univ_variables sigma in
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index a75d7c5ac..2f64fd351 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -3515,26 +3515,6 @@ let find_induction_type isrec elim hyp0 gl =
 	evd, scheme, ElimUsing (elim,indsign) in
   evd,(Option.get scheme.indref,scheme.nparams, elim)
 
-let find_induction_type_and_adjust_indarg isrec elim (c,lbind) gl =
-  let env = Proofview.Goal.env gl in
-  let sigma = Proofview.Goal.sigma gl in
-  let tmptyp = typ_of env sigma c in
-  let typ, nrealargs = match elim with
-  | None ->
-      let mind,typ = reduce_to_quantified_ind env sigma tmptyp in
-      typ, inductive_nrealargs (fst mind)
-  | Some (e,ebind as elimc) ->
-      let elimt = Typing.type_of env sigma e in
-      let scheme = compute_elim_sig ~elimc elimt in
-      if scheme.indarg = None then error "Cannot find induction type";
-      let indref = Option.get scheme.indref in
-      let typ = reduce_to_quantified_ref env sigma indref tmptyp in
-      typ, scheme.nargs in
-  let ctxt,_ = splay_prod env sigma typ in
-  let indclause = make_clenv_binding_env env sigma (c,typ) lbind in
-  let is_partial_and_ground = ctxt <> [] && is_ground_term sigma c in
-  indclause, nrealargs, is_partial_and_ground
-
 let find_elim_signature isrec elim hyp0 gl =
   compute_elim_signature (find_elim isrec elim hyp0 gl) hyp0