Diverses petites simplications de la machine de preuves.

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

6 files changed, 6 insertions, 94 deletions

diff --git a/tactics/eauto.ml b/tactics/eauto.ml
index 3928d6a5ed..01e7cca46a 100644
--- a/tactics/eauto.ml
+++ b/tactics/eauto.ml
@@ -79,36 +79,6 @@ let prolog_tac l n gl =
   with UserError ("Refiner.tclFIRST",_) ->
     errorlabstrm "Prolog.prolog" [< 'sTR "Prolog failed" >]
 
-let evars_of evc c = 
-  let rec evrec acc c =
-    match kind_of_term c with
-    | Evar (n, _) when Evd.in_dom evc n -> c :: acc
-    | _ -> fold_constr evrec acc c
-  in 
-  evrec [] c
-
-let instantiate n c gl =
-  let sigma = project gl in
-  let evl = evars_of sigma (pf_concl gl) in
-  let (wc,kONT) = startWalk gl in
-  if List.length evl < n then error "not enough evars";
-  let (n,_) as k = destEvar (List.nth evl (n-1)) in 
-  if Evd.is_defined sigma n then 
-    error "Instantiate called on already-defined evar";
-  let wc' = w_Define n c wc in 
-  kONT wc' gl
-
-let instantiate_tac = function
-  | [Integer n; Command com] ->
-      (fun gl -> instantiate n (pf_interp_constr gl com) gl)
-  | [Integer n; Constr c] ->
-      (fun gl -> instantiate n c gl)
-  | _ -> invalid_arg "Instantiate called with bad arguments"
-
-let normEvars gl =
-  let sigma = project gl in
-  convert_concl (nf_betaiota (Evarutil.nf_evar sigma (pf_concl gl))) gl
-
 let vernac_prolog =
   let uncom = function
     | Constr c -> c
@@ -123,12 +93,6 @@ let vernac_prolog =
   fun coms n -> 
     gentac ((Integer n) :: (List.map (fun com -> (Constr com)) coms))
 
-let vernac_instantiate =
-  hide_tactic "Instantiate" instantiate_tac
-
-let vernac_normevars =
-  hide_atomic_tactic "NormEvars" normEvars
-
 open Auto
 
 (***************************************************************************)
diff --git a/tactics/tacentries.ml b/tactics/tacentries.ml
index b440546609..d7397e8fcb 100644
--- a/tactics/tacentries.ml
+++ b/tactics/tacentries.ml
@@ -52,4 +52,6 @@ let v_destruct      = hide_tactic "Destruct"      dyn_destruct
 let v_new_destruct  = hide_tactic "NewDestruct"   dyn_new_destruct
 let v_fix           = hide_tactic "Fix"           dyn_mutual_fix
 let v_cofix         = hide_tactic "Cofix"         dyn_mutual_cofix
+let vernac_instantiate =
+  hide_tactic "Instantiate" Evar_refiner.instantiate_tac
 
diff --git a/tactics/tacentries.mli b/tactics/tacentries.mli
index cb5cf8385e..86ab39dfff 100644
--- a/tactics/tacentries.mli
+++ b/tactics/tacentries.mli
@@ -52,3 +52,4 @@ val v_destruct      : tactic_arg list -> tactic
 (*i val v_new_destruct  : tactic_arg list -> tactic i*)
 val v_fix           : tactic_arg list -> tactic
 val v_cofix         : tactic_arg list -> tactic
+val vernac_instantiate : tactic_arg list -> tactic
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index c9247c09e1..e7d61a79a5 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -1868,3 +1868,6 @@ let dyn_tclABSTRACT =
        | [Identifier s; Tac (tac,_)] ->
 	   tclABSTRACT (Some s) tac
        | _ -> invalid_arg "tclABSTRACT") 
+
+
+
diff --git a/tactics/wcclausenv.ml b/tactics/wcclausenv.ml
index 3b93cce073..a8d53dae9c 100644
--- a/tactics/wcclausenv.ml
+++ b/tactics/wcclausenv.ml
@@ -99,30 +99,8 @@ let clenv_constrain_with_bindings bl clause =
     in 
     matchrec clause bl
 
-let add_prod_rel sigma (t,env) =
-  match kind_of_term t with
-    | Prod (na,t1,b) ->
-        (b,push_rel_assum (na, t1) env)
-    | LetIn (na,c1,t1,b) ->
-        (b,push_rel (na,Some c1, t1) env)
-    | _ -> failwith "add_prod_rel"
-
-let rec add_prods_rel sigma (t,env) =
-  try 
-    add_prods_rel sigma (add_prod_rel sigma (whd_betadeltaiota env sigma t,env))
-  with Failure "add_prod_rel" -> 
-    (t,env)
-
 (* What follows is part of the contents of the former file tactics3.ml *)
     
-let res_pf_THEN kONT clenv tac gls =
-  let clenv' = (clenv_unique_resolver false clenv gls) in 
-  (tclTHEN (clenv_refine kONT clenv') (tac clenv')) gls
-
-let res_pf_THEN_i kONT clenv tac gls =
-  let clenv' = (clenv_unique_resolver false clenv gls) in 
-  tclTHEN_i (clenv_refine kONT clenv') (tac clenv') gls
-
 let elim_res_pf_THEN_i kONT clenv tac gls =  
   let clenv' = (clenv_unique_resolver true clenv gls) in
   tclTHEN_i (clenv_refine kONT clenv') (tac clenv') gls
@@ -185,21 +163,3 @@ let applyUsing c gl =
   let clause = mk_clenv_using wc c in 
   res_pf kONT clause gl
 
-let clenv_apply_n_times n ce =
-  let templtyp = clenv_instance_template_type ce
-  and templval = (clenv_template ce).rebus in   
-  let rec apprec ce argacc (n,ty) =
-    let env = Global.env () in
-    let templtyp = whd_betadeltaiota env (w_Underlying ce.hook) ty in
-    match (n, kind_of_term templtyp) with 
-      | (0, _) ->
-	  clenv_change_head (applist(templval,List.rev argacc), templtyp) ce
-      | (n, Prod (na,dom,rng)) ->
-          let mv = new_meta() in
-          let newce = clenv_pose (na,mv,dom) ce in
-	  apprec newce (mkMeta mv::argacc) (n-1, subst1 (mkMeta mv) rng)
-      | (n, LetIn (na,b,t,c)) ->
-	  apprec ce argacc (n, subst1 b c)
-      | (n, _) -> failwith "clenv_apply_n_times"
-  in 
-  apprec ce [] (n, templtyp)
diff --git a/tactics/wcclausenv.mli b/tactics/wcclausenv.mli
index 24174e5082..26c46e89a5 100644
--- a/tactics/wcclausenv.mli
+++ b/tactics/wcclausenv.mli
@@ -36,9 +36,6 @@ type wc = named_context sigma
 
 val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv
 
-val add_prod_rel : evar_map -> constr * env -> constr * env
-val add_prods_rel : evar_map -> constr * env -> constr * env
-
 (*i**
 val add_prod_sign : 
   'a evar_map -> constr * types signature -> constr * types signature
@@ -47,22 +44,7 @@ val add_prods_sign :
   'a evar_map -> constr * types signature -> constr * types signature
 **i*)
 
-val res_pf_THEN : 
-  (wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic) -> tactic
-
-(* This behaves as [res_pf_THEN] but the tactic applied then takes
-   also the subgoal number (starting from 1) as argument *)
-val res_pf_THEN_i : 
-  (wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) -> tactic
-
 val elim_res_pf_THEN_i : 
   (wc -> tactic) -> wc clausenv -> (wc clausenv -> int -> tactic) -> tactic
 
-val mk_clenv_using : wc -> constr -> wc clausenv
-
 val applyUsing : constr -> tactic
-
-val clenv_apply_n_times : int -> wc clausenv -> wc clausenv
-
-
-