Imported Upstream version 8.0pl3upstream/8.0pl3

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;