From 29863a4dc9feeb75a184587b7b994626db7b94ce Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 8 Jun 2008 20:24:51 +0000
Subject: - Patch sur "intros until 0" - MAJ CHANGES et COMPATIBILITY -
 Réservation de || et && dans Notations.v - code mort et MAJ suite commit
 11072 (tactics.ml et changes.txt)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11073 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/tactics.ml | 22 ----------------------
 1 file changed, 22 deletions(-)

(limited to 'tactics')

diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c81d7f3172..905511b120 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1154,28 +1154,6 @@ let generalize_goal gl i ((occs,c),na) cl =
   let na = generalized_name c t cl' na in
   mkProd (na,t,cl')
 
-(*
-  match kind_of_term cl with
-  | App (f,[|a|]) when isLambda f & eq_constr a c ->
-      (* Assume tactic pattern has been applied first *)
-      let na = match kind_of_term c with Var id -> Name id | _ -> Anonymous in
-      mkProd_name (pf_env gl) (na,t,mkApp (f,[|mkRel 1|]))
-  | _ ->
-    match kind_of_term c with
-    | Var id ->
-	(* The choice of remembering or not a non dependent name has an impact
-	   on the future Intro naming strategy! *)
-	(* if dependent c cl then mkNamedProd id t cl
-	   else mkProd (Anonymous,t,cl) *)
- 	mkNamedProd id t cl
-    | _        -> 
-        let cl' = subst_term c cl in
-        if noccurn 1 cl' then 
-	  mkProd (Anonymous,t,cl)
-        else
-	  mkProd_name (pf_env gl) (Anonymous, t, cl')
-*)
-
 let generalize_dep c gl =
   let env = pf_env gl in
   let sign = pf_hyps gl in
-- 
cgit v1.2.3