From a9adcb3941900c416f106ddac6fd646603b335b8 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 26 Oct 2014 22:33:45 +0100
Subject: Dead code

---
 parsing/g_tactic.ml4     | 7 -------
 pretyping/unification.ml | 2 +-
 2 files changed, 1 insertion(+), 8 deletions(-)

diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 25dd0db453..fb09a31085 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -619,13 +619,6 @@ GEXTEND Gram
           l = LIST0 [","; c = pattern_occ; na = as_name -> (c,na)] ->
           TacAtom (!@loc, TacGeneralize (((nl,c),na)::l))
       | IDENT "generalize"; IDENT "dependent"; c = constr -> TacAtom (!@loc, TacGeneralizeDep c)
-(* Towards a "generalize in" which generalize in place: problem: this is somehow inconsistent with "generalize at" (from 8.2) which is not in place.
-      | IDENT "generalize"; c = constr; "in"; cl = in_clause;
-          na = as_name;
-          l = LIST0 [","; c = constr; "in"; cl = in_clause; na = as_name ->
-            ((cl,c),na)] ->
-          TacGeneralize (true,((cl,c),na)::l)
-*)
 
       (* Derived basic tactics *)
       | IDENT "induction"; ic = induction_clause_list ->
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 1a1d03cc8a..07940bf57d 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1480,7 +1480,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
             ++ str ".")
         else
           (push_named_context_val d sign,depdecls)
-    | (AtOccs (AllOccurrences, InHyp) | LikeFirst) as occ ->
+    | (AtOccs (AllOccurrences, InHyp) | LikeFirst) ->
         let newdecl = replace_term_occ_decl_modulo LikeFirst test mkvarid d in
         if Context.eq_named_declaration d newdecl
            && not (indirectly_dependent c d depdecls)
-- 
cgit v1.2.3