diff options
| -rw-r--r-- | kernel/environ.ml | 24 | ||||
| -rw-r--r-- | kernel/environ.mli | 1 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 6 | ||||
| -rw-r--r-- | proofs/tacexpr.ml | 1 | ||||
| -rw-r--r-- | tactics/evar_tactics.ml | 12 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 18 |
6 files changed, 8 insertions, 54 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml index 2d821991e..56c057488 100644 --- a/kernel/environ.ml +++ b/kernel/environ.ml @@ -245,30 +245,6 @@ let global_vars_set env constr = in filtrec Idset.empty constr -(* like [global_vars] but don't get through evars *) -let global_vars_set_drop_evar env constr = - let fold_constr_drop_evar f acc c = match kind_of_term c with - | (Rel _ | Meta _ | Var _ | Sort _ | Const _ | Ind _ - | Construct _) -> acc - | Cast (c,_,t) -> f (f acc c) t - | Prod (_,t,c) -> f (f acc t) c - | Lambda (_,t,c) -> f (f acc t) c - | LetIn (_,b,t,c) -> f (f (f acc b) t) c - | App (c,l) -> Array.fold_left f (f acc c) l - | Evar (_,l) -> acc - | Case (_,p,c,bl) -> Array.fold_left f (f (f acc p) c) bl - | Fix (_,(lna,tl,bl)) -> - let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in - Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd - | CoFix (_,(lna,tl,bl)) -> - let fd = array_map3 (fun na t b -> (na,t,b)) lna tl bl in - Array.fold_left (fun acc (na,t,b) -> f (f acc t) b) acc fd in - let rec filtrec acc c = - let vl = vars_of_global env c in - let acc = List.fold_right Idset.add vl acc in - fold_constr_drop_evar filtrec acc c - in - filtrec Idset.empty constr (* [keep_hyps env ids] keeps the part of the section context of [env] which contains the variables of the set [ids], and recursively the variables diff --git a/kernel/environ.mli b/kernel/environ.mli index 175b18b24..8ba5962d3 100644 --- a/kernel/environ.mli +++ b/kernel/environ.mli @@ -165,7 +165,6 @@ val set_engagement : engagement -> env -> env (* [global_vars_set env c] returns the list of [id]'s occurring as [VAR id] in [c] *) val global_vars_set : env -> constr -> Idset.t -val global_vars_set_drop_evar : env -> constr -> Idset.t (* the constr must be an atomic construction *) val vars_of_global : env -> constr -> identifier list diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index a76402e09..0eab3f7f9 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -350,12 +350,6 @@ GEXTEND Gram | IDENT "cut"; c = constr -> TacCut c | IDENT "generalize"; lc = LIST1 constr -> TacGeneralize lc | IDENT "generalize"; IDENT "dependent"; c = constr -> TacGeneralizeDep c - (* | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")"; "in"; - hid = hypident -> - let (id,(hloc,_)) = hid in - TacInstantiate (n,c,HypLocation (id,hloc)) - | IDENT "instantiate"; "("; n = natural; ":="; c = lconstr; ")" -> - TacInstantiate (n,c,ConclLocation ()) *) | IDENT "specialize"; n = OPT natural; lcb = constr_with_bindings -> TacSpecialize (n,lcb) diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml index b072e7cc3..caa7523a6 100644 --- a/proofs/tacexpr.ml +++ b/proofs/tacexpr.ml @@ -136,7 +136,6 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr = | TacGeneralize of 'constr list | TacGeneralizeDep of 'constr | TacLetTac of name * 'constr * 'id gclause -(* | TacInstantiate of int * 'constr * (('id * hyp_location_flag,unit) location) *) (* Derived basic tactics *) | TacSimpleInduction of quantified_hypothesis diff --git a/tactics/evar_tactics.ml b/tactics/evar_tactics.ml index 6339ed536..f3454b711 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 8eff3ccd9..799361a27 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) |