summaryrefslogtreecommitdiff
path: root/tactics/tacinterp.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tactics/tacinterp.ml')
-rw-r--r--tactics/tacinterp.ml37
1 files changed, 17 insertions, 20 deletions
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 4f8e7d7c..245b5a5b 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tacinterp.ml,v 1.84.2.8 2005/01/15 14:56:54 herbelin Exp $ *)
+(* $Id: tacinterp.ml,v 1.84.2.11 2005/11/04 09:01:27 herbelin Exp $ *)
open Constrintern
open Closure
@@ -440,20 +440,18 @@ let intern_constr_reference strict ist = function
let loc,qid = qualid_of_reference r in
RRef (loc,locate_reference qid), if strict then None else Some (CRef r)
-let intern_reference strict ist = function
- | Ident (loc,id) when is_atomic id -> Tacexp (lookup_atomic id)
- | r ->
- (try Reference (intern_tac_ref ist r)
+let intern_reference strict ist r =
+ (try Reference (intern_tac_ref ist r)
+ with Not_found ->
+ (try
+ ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
with Not_found ->
- (try
- ConstrMayEval (ConstrTerm (intern_constr_reference strict ist r))
- with Not_found ->
- (match r with
- | Ident (loc,id) when not strict ->
- IntroPattern (IntroIdentifier id)
- | _ ->
- let (loc,qid) = qualid_of_reference r in
- error_global_not_found_loc loc qid)))
+ (match r with
+ | Ident (loc,id) when is_atomic id -> Tacexp (lookup_atomic id)
+ | Ident (loc,id) when not strict -> IntroPattern (IntroIdentifier id)
+ | _ ->
+ let (loc,qid) = qualid_of_reference r in
+ error_global_not_found_loc loc qid)))
let rec intern_intro_pattern lf ist = function
| IntroOrAndPattern l ->
@@ -668,12 +666,12 @@ let rec intern_atomic lf ist x =
(* Automation tactics *)
| TacTrivial l -> TacTrivial l
- | TacAuto (n,l) -> TacAuto (n,l)
+ | TacAuto (n,l) -> TacAuto (option_app (intern_int_or_var ist) n,l)
| TacAutoTDB n -> TacAutoTDB n
| TacDestructHyp (b,id) -> TacDestructHyp(b,intern_hyp ist id)
| TacDestructConcl -> TacDestructConcl
| TacSuperAuto (n,l,b1,b2) -> TacSuperAuto (n,l,b1,b2)
- | TacDAuto (n,p) -> TacDAuto (n,p)
+ | TacDAuto (n,p) -> TacDAuto (option_app (intern_int_or_var ist) n,p)
(* Derived basic tactics *)
| TacSimpleInduction (h,ids) ->
@@ -1558,8 +1556,7 @@ and interp_match_context ist g lr lmr =
| e when is_match_catchable e ->
apply_match_context ist env goal (nrs+1) (List.tl lex) tl))
| _ ->
- errorlabstrm "Tacinterp.apply_match_context" (str
- "No matching clauses for match goal")
+ errorlabstrm "Tacinterp.apply_match_context"
(v 0 (str "No matching clauses for match goal" ++
(if ist.debug=DebugOff then
fnl() ++ str "(use \"Debug On\" for more info)"
@@ -1744,12 +1741,12 @@ and interp_atomic ist gl = function
(* Automation tactics *)
| TacTrivial l -> Auto.h_trivial l
- | TacAuto (n, l) -> Auto.h_auto n l
+ | TacAuto (n, l) -> Auto.h_auto (option_app (interp_int_or_var ist) n) l
| TacAutoTDB n -> Dhyp.h_auto_tdb n
| TacDestructHyp (b,id) -> Dhyp.h_destructHyp b (interp_hyp ist gl id)
| TacDestructConcl -> Dhyp.h_destructConcl
| TacSuperAuto (n,l,b1,b2) -> Auto.h_superauto n l b1 b2
- | TacDAuto (n,p) -> Auto.h_dauto (n,p)
+ | TacDAuto (n,p) -> Auto.h_dauto (option_app (interp_int_or_var ist) n,p)
(* Derived basic tactics *)
| TacSimpleInduction (h,ids) ->