summaryrefslogtreecommitdiff
path: root/tactics
diff options
context:
space:
mode:
Diffstat (limited to 'tactics')
-rw-r--r--tactics/auto.ml10
-rw-r--r--tactics/inv.ml17
-rw-r--r--tactics/tacinterp.ml37
-rw-r--r--tactics/tactics.ml14
4 files changed, 44 insertions, 34 deletions
diff --git a/tactics/auto.ml b/tactics/auto.ml
index b530178e..d7130f35 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: auto.ml,v 1.63.2.2 2004/12/06 11:25:21 herbelin Exp $ *)
+(* $Id: auto.ml,v 1.63.2.3 2005/05/15 12:47:04 herbelin Exp $ *)
open Pp
open Util
@@ -812,7 +812,10 @@ let gen_auto n dbnames =
| None -> full_auto n
| Some l -> auto n l
-let h_auto n l = Refiner.abstract_tactic (TacAuto (n,l)) (gen_auto n l)
+let inj_or_var = option_app (fun n -> Genarg.ArgArg n)
+
+let h_auto n l =
+ Refiner.abstract_tactic (TacAuto (inj_or_var n,l)) (gen_auto n l)
(**************************************************************************)
(* The "destructing Auto" from Eduardo *)
@@ -839,7 +842,8 @@ let dauto = function
| Some n, Some p -> dautomatic p n
| None, Some p -> dautomatic p !default_search_depth
-let h_dauto (n,p) = Refiner.abstract_tactic (TacDAuto (n,p)) (dauto (n,p))
+let h_dauto (n,p) =
+ Refiner.abstract_tactic (TacDAuto (inj_or_var n,p)) (dauto (n,p))
(***************************************)
(*** A new formulation of Auto *********)
diff --git a/tactics/inv.ml b/tactics/inv.ml
index 54ce467c..e4bab195 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: inv.ml,v 1.53.2.1 2004/07/16 19:30:53 herbelin Exp $ *)
+(* $Id: inv.ml,v 1.53.2.3 2005/09/08 12:28:00 herbelin Exp $ *)
open Pp
open Util
@@ -135,9 +135,8 @@ let make_inv_predicate env sigma indf realargs id status concl =
else
make_iterated_tuple env' sigma (ai,ati) (xi,ti)
in
- let type_type_rhs = get_sort_of env sigma (type_of env sigma rhs) in
let sort = get_sort_of env sigma concl in
- let eq_term = find_eq_pattern type_type_rhs sort in
+ let eq_term = Coqlib.build_coq_eq () in
let eqn = applist (eq_term ,[eqnty;lhs;rhs]) in
build_concl ((Anonymous,lift n eqn)::eqns) (n+1) restlist
in
@@ -191,12 +190,14 @@ let make_inv_predicate env sigma indf realargs id status concl =
and introduces generalized hypotheis.
Precondition: t=(mkVar id) *)
-let rec dependent_hyps id idlist sign =
+let rec dependent_hyps id idlist gl =
let rec dep_rec =function
| [] -> []
- | (id1,_,id1ty as d1)::l ->
- if occur_var (Global.env()) id id1ty
- then d1 :: dep_rec l
+ | (id1,_,_)::l ->
+ (* Update the type of id1: it may have been subject to rewriting *)
+ let d = pf_get_hyp gl id1 in
+ if occur_var_in_decl (Global.env()) id d
+ then d :: dep_rec l
else dep_rec l
in
dep_rec idlist
@@ -281,7 +282,7 @@ Nota: with Inversion_clear, only four useless hypotheses
*)
let generalizeRewriteIntros tac depids id gls =
- let dids = dependent_hyps id depids (pf_env gls) in
+ let dids = dependent_hyps id depids gls in
(tclTHENSEQ
[bring_hyps dids; tac;
(* may actually fail to replace if dependent in a previous eq *)
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) ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index b6eaf015..2ba09e52 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -6,7 +6,7 @@
(* * GNU Lesser General Public License Version 2.1 *)
(************************************************************************)
-(* $Id: tactics.ml,v 1.162.2.4 2004/12/04 10:26:46 herbelin Exp $ *)
+(* $Id: tactics.ml,v 1.162.2.7 2005/07/13 16:18:57 herbelin Exp $ *)
open Pp
open Util
@@ -220,8 +220,16 @@ let pattern_option l = reduct_option (pattern_occs l)
(* A function which reduces accordingly to a reduction expression,
as the command Eval does. *)
+let needs_check = function
+ (* Expansion is not necessarily well-typed: e.g. expansion of t into x is
+ not well-typed in [H:(P t); x:=t |- G] because x is defined after H *)
+ | Fold _ -> true
+ | _ -> false
+
let reduce redexp cl goal =
- redin_combinator (reduction_of_redexp redexp) cl goal
+ (if needs_check redexp then with_check else (fun x -> x))
+ (redin_combinator (reduction_of_redexp redexp) cl)
+ goal
(* Unfolding occurrences of a constant *)
@@ -741,7 +749,7 @@ let letin_tac with_eq name c occs gl =
if not (mem_named_context x (pf_hyps gl)) then x else
error ("The variable "^(string_of_id x)^" is already declared") in
let (depdecls,lastlhyp,ccl)= letin_abstract id c occs gl in
- let t = pf_type_of gl c in
+ let t = Evarutil.refresh_universes (pf_type_of gl c) in
let newcl = mkNamedLetIn id c t ccl in
tclTHENLIST
[ convert_concl_no_check newcl;
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-09 05:35:01 +0000