Removing the legacy intro tactic code.

5 files changed, 0 insertions, 29 deletions

diff --git a/proofs/logic.ml b/proofs/logic.ml
index aa99dd036e..b7a33cdba8 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -522,26 +522,6 @@ let prim_refiner r sigma goal =
   in
   match r with
     (* Logical rules *)
-    | Intro id ->
-    	if !check && mem_named_context id (named_context_of_val sign) then
-	  error ("Variable " ^ Id.to_string id ^ " is already declared.");
-        (match kind_of_term (strip_outer_cast cl) with
-	   | Prod (_,c1,b) ->
-	       let (sg,ev,sigma) = mk_goal (push_named_context_val (id,None,c1) sign)
-			  (subst1 (mkVar id) b) in
-               let sigma = 
-		 Goal.V82.partial_solution_to sigma goal sg (mkNamedLambda id c1 ev) in
-	       ([sg], sigma)
-	   | LetIn (_,c1,t1,b) ->
-	       let (sg,ev,sigma) =
-		 mk_goal (push_named_context_val (id,Some c1,t1) sign)
-		   (subst1 (mkVar id) b) in
-	       let sigma = 
-		 Goal.V82.partial_solution_to sigma goal sg (mkNamedLetIn id c1 t1 ev) in
-	       ([sg], sigma)
-	   | _ ->
-	       raise (RefinerError IntroNeedsProduct))
-
     | Cut (b,replace,id,t) ->
 (*        if !check && not (Retyping.get_sort_of env sigma t) then*)
         let (sg1,ev1,sigma) = mk_goal sign (nf_betaiota sigma t) in
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index d7e1c7b531..613f85a731 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -27,7 +27,6 @@ type goal = Goal.goal
 type tactic = goal sigma -> goal list sigma 
 
 type prim_rule =
-  | Intro of Id.t
   | Cut of bool * bool * Id.t * types
   | FixRule of Id.t * int * (Id.t * int * constr) list * int
   | Cofix of Id.t * (Id.t * constr) list * int
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 2225a6e304..9361d48e61 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -19,7 +19,6 @@ open Misctypes
    is used by [Proof_tree] and [Refiner] *)
 
 type prim_rule =
-  | Intro of Id.t
   | Cut of bool * bool * Id.t * types
   | FixRule of Id.t * int * (Id.t * int * constr) list * int
   | Cofix of Id.t * (Id.t * constr) list * int
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 5b36052244..03f2fd2b44 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -105,10 +105,6 @@ let pf_matches                  = pf_apply ConstrMatching.matches_conv
 
 let refiner = refiner
 
-(* This does not check that the variable name is not here *)
-let introduction_no_check id =
-  refiner (Intro id)
-
 let internal_cut_no_check replace id t gl =
   refiner (Cut (true,replace,id,t)) gl
 
@@ -133,7 +129,6 @@ let mutual_cofix f others j gl =
 
 (* Versions with consistency checks *)
 
-let introduction id    = with_check (introduction_no_check id)
 let internal_cut b d t = with_check (internal_cut_no_check b d t)
 let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t)
 let refine c           = with_check (refine_no_check c)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index a9f7bffbff..8b95ae4273 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -84,7 +84,6 @@ val pf_is_matching : goal sigma -> constr_pattern -> constr -> bool
 (** {6 The most primitive tactics. } *)
 
 val refiner                   : rule -> tactic
-val introduction_no_check     : Id.t -> tactic
 val internal_cut_no_check     : bool -> Id.t -> types -> tactic
 val refine_no_check           : constr -> tactic
 val thin_no_check             : Id.t list -> tactic
@@ -94,7 +93,6 @@ val mutual_cofix    : Id.t -> (Id.t * constr) list -> int -> tactic
 
 (** {6 The most primitive tactics with consistency and type checking } *)
 
-val introduction     : Id.t -> tactic
 val internal_cut     : bool -> Id.t -> types -> tactic
 val internal_cut_rev : bool -> Id.t -> types -> tactic
 val refine           : constr -> tactic