Suppression de code mort

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9582 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 8 insertions, 22 deletions

diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml
index 6339ed5363..f3454b711b 100644
--- a/tactics/evar_tactics.ml
+++ b/tactics/evar_tactics.ml
@@ -38,21 +38,21 @@ let instantiate n rawc ido gl =
 	    match hloc with
 		InHyp ->  
 		  (match decl with 
-		       (_,None,typ) -> evar_list sigma typ
-		     | _ -> error 
-			 "please be more specific : in type or value ?")
+		      (_,None,typ) -> evar_list sigma typ
+		    | _ -> error 
+			"please be more specific : in type or value ?")
 	      | InHypTypeOnly ->
 		  let (_, _, typ) = decl in evar_list sigma typ
 	      | InHypValueOnly ->
 		  (match decl with 
-		       (_,Some body,_) -> evar_list sigma body
-		     | _ -> error "not a let .. in  hypothesis") in
+		      (_,Some body,_) -> evar_list sigma body
+		    | _ -> error "not a let .. in  hypothesis") in
     if List.length evl < n then
       error "not enough uninstantiated existential variables";
     if n <= 0 then error "incorrect existential variable index";
     let ev,_ =  destEvar (List.nth evl (n-1)) in
     let evd' = w_refine ev rawc (create_evar_defs sigma)  in
-    Refiner.tclEVARS (evars_of evd') gl
+      Refiner.tclEVARS (evars_of evd') gl
 	
 (*
 let pfic gls c =
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 8eff3ccd98..799361a27d 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -653,13 +653,6 @@ let rec intern_atomic lf ist x =
       let na = intern_name lf ist na in
       TacLetTac (na,intern_constr ist c,
                  (clause_app (intern_hyp_location ist) cls))
-(*  | TacInstantiate (n,c,idh) -> 
-      TacInstantiate (n,intern_constr ist c,
-		      (match idh with
-			   ConclLocation () -> ConclLocation ()
-			 | HypLocation (id,hloc) -> 
-			      HypLocation(intern_hyp_or_metaid ist id,hloc))) 
-*)
 
   (* Automation tactics *)
   | TacTrivial (lems,l) -> TacTrivial (List.map (intern_constr ist) lems,l)
@@ -2020,13 +2013,7 @@ and interp_atomic ist gl = function
   | TacLetTac (na,c,clp) ->
       let clp = interp_clause ist gl clp in
       h_let_tac (interp_name ist gl na) (pf_interp_constr ist gl c) clp
-(* | TacInstantiate (n,c,idh) -> h_instantiate n (fst c) 
-      (* pf_interp_constr ist gl c *)
-      (match idh with
-	   ConclLocation () -> ConclLocation ()
-	 | HypLocation (id,hloc) -> 
-	     HypLocation(interp_hyp ist gl id,hloc))
-*)
+
   (* Automation tactics *)
   | TacTrivial (lems,l) -> 
       Auto.h_trivial (pf_interp_constr_list ist gl lems)
@@ -2341,8 +2328,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with
   | TacGeneralize cl -> TacGeneralize (List.map (subst_rawconstr subst) cl)
   | TacGeneralizeDep c -> TacGeneralizeDep (subst_rawconstr subst c)
   | TacLetTac (id,c,clp) -> TacLetTac (id,subst_rawconstr subst c,clp)
-(*| TacInstantiate (n,c,ido) -> TacInstantiate (n,subst_rawconstr subst c,ido)
-*)
+
   (* Automation tactics *)
   | TacTrivial (lems,l) -> TacTrivial (List.map (subst_rawconstr subst) lems,l)
   | TacAuto (n,lems,l) -> TacAuto (n,List.map (subst_rawconstr subst) lems,l)