diff options
Diffstat (limited to 'tactics/tacinterp.ml')
| -rw-r--r-- | tactics/tacinterp.ml | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 2b2f39e1e..4a395fa31 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -663,12 +663,13 @@ 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,c,idh) -> TacInstantiate (n,intern_constr ist c, (match idh with ConclLocation () -> ConclLocation () | HypLocation (id,hloc) -> - HypLocation(intern_hyp_or_metaid ist id,hloc))) + HypLocation(intern_hyp_or_metaid ist id,hloc))) +*) (* Automation tactics *) | TacTrivial l -> TacTrivial l @@ -1717,13 +1718,13 @@ and interp_atomic ist gl = function | TacLetTac (na,c,clp) -> let clp = interp_clause ist gl clp in h_let_tac (interp_name ist na) (pf_interp_constr ist gl c) clp - | TacInstantiate (n,c,idh) -> h_instantiate n (fst c) +(* | 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 l -> Auto.h_trivial l | TacAuto (n, l) -> Auto.h_auto n l @@ -1976,8 +1977,8 @@ 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) - +(*| TacInstantiate (n,c,ido) -> TacInstantiate (n,subst_rawconstr subst c,ido) +*) (* Automation tactics *) | TacTrivial l -> TacTrivial l | TacAuto (n,l) -> TacAuto (n,l) |