Imported Upstream version 8.0pl2upstream/8.0pl2

13 files changed, 151 insertions, 129 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index d087420a..b530178e 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.1 2004/07/16 19:30:51 herbelin Exp $ *)
+(* $Id: auto.ml,v 1.63.2.2 2004/12/06 11:25:21 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -199,8 +199,12 @@ let make_apply_entry env sigma (eapply,verbose) name (c,cty) =
         in 
 	if eapply & (nmiss <> 0) then begin
           if verbose then 
+	    if !Options.v7 then
 	    warn (str "the hint: EApply " ++ prterm c ++
-		    str " will only be used by EAuto"); 
+		    str " will only be used by EAuto")
+	    else
+	    warn (str "the hint: eapply " ++ prterm c ++
+		    str " will only be used by eauto"); 
           (hd,
            { hname = name;
 	     pri = nb_hyp cty + nmiss;
@@ -281,40 +285,8 @@ let add_hint dbname hintlist =
 
 let cache_autohint (_,(local,name,hintlist)) = add_hint name hintlist
 
-(*  let recalc_hints hintlist =
-    let env = Global.env() and sigma = Evd.empty in
-    let recalc_hint ((_,data) as hint) =
-      match data.code with
-	| Res_pf (c,_) ->
-	    let c' = Term.subst_mps subst c in
-	      if c==c' then hint else
-		make_apply_entry env sigma (false,false) 
-		  data.hname (c', type_of env sigma c')
-	| ERes_pf (c,_) ->
-	    let c' = Term.subst_mps subst c in
-	      if c==c' then hint else
-		make_apply_entry env sigma (true,false) 
-		  data.hname (c', type_of env sigma c')
-	| Give_exact c ->
-	    let c' = Term.subst_mps subst c in
-	      if c==c' then hint else
-		make_exact_entry data.hname (c',type_of env sigma c')
-	| Res_pf_THEN_trivial_fail (c,_) ->
-	    let c' = Term.subst_mps subst c in
-	      if c==c' then hint else
-		make_trivial env sigma (data.hname,c')
-	| Unfold_nth ref -> 
-	    let ref' = subst_global subst ref in
-	      if ref==ref' then hint else
-		make_unfold (data.hname,ref')
-	| Extern _ ->
-	    anomaly "Extern hints cannot be substituted!!!"
-    in
-      list_smartmap recalc_hint hintlist
-*)
-
 let forward_subst_tactic = 
-  ref (fun _ -> failwith "subst_tactic is not installed for Auto")
+  ref (fun _ -> failwith "subst_tactic is not installed for auto")
 
 let set_extern_subst_tactic f = forward_subst_tactic := f
 
@@ -430,7 +402,7 @@ let add_trivials env sigma l local dbnames =
     dbnames
 
 let forward_intern_tac = 
-  ref (fun _ -> failwith "intern_tac is not installed for Auto")
+  ref (fun _ -> failwith "intern_tac is not installed for auto")
 
 let set_extern_intern_tac f = forward_intern_tac := f
 
@@ -492,7 +464,9 @@ let add_hints local dbnames0 h =
 (*                    Functions for printing the hints                    *)
 (**************************************************************************)
 
-let fmt_autotactic = function
+let fmt_autotactic =
+  if !Options.v7 then
+  function
   | Res_pf (c,clenv) -> (str"Apply " ++ prterm c)
   | ERes_pf (c,clenv) -> (str"EApply " ++ prterm c)
   | Give_exact c -> (str"Exact " ++ prterm c)
@@ -500,6 +474,16 @@ let fmt_autotactic = function
       (str"Apply " ++ prterm c ++ str" ; Trivial")
   | Unfold_nth c -> (str"Unfold " ++  pr_global c)
   | Extern tac -> (str "Extern " ++ Pptactic.pr_glob_tactic tac)
+  else
+  function
+  | Res_pf (c,clenv) -> (str"apply " ++ prterm c)
+  | ERes_pf (c,clenv) -> (str"eapply " ++ prterm c)
+  | Give_exact c -> (str"exact " ++ prterm c)
+  | Res_pf_THEN_trivial_fail (c,clenv) -> 
+      (str"apply " ++ prterm c ++ str" ; trivial")
+  | Unfold_nth c -> (str"unfold " ++  pr_global c)
+  | Extern tac -> 
+      (str "(external) " ++ Pptacticnew.pr_glob_tactic (Global.env()) tac)
 
 let fmt_hint v =
   (fmt_autotactic v.code ++ str"(" ++ int v.pri ++ str")" ++ spc ())
@@ -631,7 +615,7 @@ si après Intros la conclusion matche le pattern.
 (* conclPattern doit échouer avec error car il est rattraper par tclFIRST *)
 
 let forward_interp_tactic = 
-  ref (fun _ -> failwith "interp_tactic is not installed for Auto")
+  ref (fun _ -> failwith "interp_tactic is not installed for auto")
 
 let set_extern_interp f = forward_interp_tactic := f
 
@@ -700,7 +684,10 @@ let trivial dbnames gl =
 	 try 
 	   searchtable_map x
 	 with Not_found -> 
-	   error ("Trivial: "^x^": No such Hint database"))
+	   if !Options.v7 then
+	     error ("Trivial: "^x^": No such Hint database")
+	   else
+	     error ("trivial: "^x^": No such Hint database"))
       ("core"::dbnames) 
   in
   tclTRY (trivial_fail_db db_list (make_local_hint_db gl)) gl 
@@ -799,7 +786,10 @@ let auto n dbnames gl =
 	 try 
 	   searchtable_map x
 	 with Not_found -> 
-	   error ("Auto: "^x^": No such Hint database"))
+	   if !Options.v7 then
+	     error ("Auto: "^x^": No such Hint database")
+	   else
+	     error ("auto: "^x^": No such Hint database"))
       ("core"::dbnames) 
   in
   let hyps = pf_hyps gl in
diff --git a/tactics/auto.mli b/tactics/auto.mli
index ef6b85ea..ec8c0d71 100644
--- a/tactics/auto.mli
+++ b/tactics/auto.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: auto.mli,v 1.22.2.1 2004/07/16 19:30:51 herbelin Exp $ i*)
+(*i $Id: auto.mli,v 1.22.2.2 2005/01/21 16:41:52 herbelin Exp $ i*)
 
 (*i*)
 open Util
@@ -105,7 +105,7 @@ val make_resolves :
 
 (* [make_resolve_hyp hname htyp].
    used to add an hypothesis to the local hint database;
-   Never raises an User_exception;
+   Never raises a user exception;
    If the hyp cannot be used as a Hint, the empty list is returned. *)
 
 val make_resolve_hyp : 
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 7c134b89..5706e134 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -22,7 +22,7 @@ open Vernacinterp
 open Tacexpr
 
 (* Rewriting rules *)
-type rew_rule = constr * bool * tactic
+type rew_rule = constr * bool * glob_tactic_expr
 
 (* Summary and Object declaration *)
 let rewtab =
@@ -39,7 +39,6 @@ let _ =
       Summary.survive_module = false;
       Summary.survive_section   = false }
 
-(* Rewriting rules before tactic interpretation *)
 type raw_rew_rule = constr * bool * raw_tactic_expr
 
 (* Applies all the rules of one base *)
@@ -51,6 +50,7 @@ let one_base tac_main bas =
       errorlabstrm "AutoRewrite" 
         (str ("Rewriting base "^(bas)^" does not exist"))
   in
+  let lrul = List.map (fun (c,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrul in
     tclREPEAT_MAIN (tclPROGRESS (List.fold_left (fun tac (csr,dir,tc) ->
       tclTHEN tac
         (tclREPEAT_MAIN 
@@ -65,12 +65,11 @@ let autorewrite tac_main lbas =
 
 (* Functions necessary to the library object declaration *)
 let cache_hintrewrite (_,(rbase,lrl)) =
-  let l = List.rev_map (fun (c,b,t) -> (c,b,Tacinterp.eval_tactic t)) lrl in
   let l = 
     try 
-      List.rev_append l (Stringmap.find rbase !rewtab) 
+      lrl @ Stringmap.find rbase !rewtab
     with
-      | Not_found -> List.rev l
+      | Not_found -> lrl
   in
     rewtab:=Stringmap.add rbase l !rewtab
 
diff --git a/tactics/equality.ml b/tactics/equality.ml
index dd9054f5..994abb9d 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: equality.ml,v 1.120.2.1 2004/07/16 19:30:53 herbelin Exp $ *)
+(* $Id: equality.ml,v 1.120.2.4 2004/11/21 22:24:09 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -18,6 +18,7 @@ open Termops
 open Inductive
 open Inductiveops
 open Environ
+open Libnames
 open Reductionops
 open Instantiate
 open Typeops
@@ -327,8 +328,11 @@ let descend_then sigma env head dirn =
   (dirn_nlams,
    dirn_env,
    (fun dirnval (dfltval,resty) ->
-      let arign,_ = get_arity env indf in
-      let p = it_mkLambda_or_LetIn (lift mip.mind_nrealargs resty) arign in
+      let arsign,_ = get_arity env indf in
+      let depind = build_dependent_inductive env indf in
+      let deparsign = (Anonymous,None,depind)::arsign in
+      let p =
+	it_mkLambda_or_LetIn (lift (mip.mind_nrealargs+1) resty) deparsign in
       let build_branch i =
 	let result = if i = dirn then dirnval else dfltval in
 	it_mkLambda_or_LetIn_name env result cstr.(i-1).cs_args in
@@ -371,7 +375,9 @@ let construct_discriminator sigma env dirn c sort =
   let (mib,mip) = lookup_mind_specif env ind in
   let arsign,arsort = get_arity env indf in
   let (true_0,false_0,sort_0) = build_coq_True(),build_coq_False(),Prop Null in
-  let p = it_mkLambda_or_LetIn (mkSort sort_0) arsign in
+  let depind = build_dependent_inductive env indf in
+  let deparsign = (Anonymous,None,depind)::arsign in
+  let p = it_mkLambda_or_LetIn (mkSort sort_0) deparsign in
   let cstrs = get_constructors env indf in
   let build_branch i =
     let endpt = if i = dirn then true_0 else false_0 in
@@ -419,14 +425,8 @@ let discrimination_pf e (t,t1,t2) discriminator lbeq gls =
 
 exception NotDiscriminable
 
-let discr id gls =
-  let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in
+let discrEq (lbeq,(t,t1,t2)) id gls =
   let sort = pf_type_of gls (pf_concl gls) in 
-  let (lbeq,(t,t1,t2)) =
-    try find_eq_data_decompose eqn
-    with PatternMatchingFailure ->
-      errorlabstrm "discr" (pr_id id ++ str": not a primitive equality here")
-  in
   let sigma = project gls in
   let env = pf_env gls in
   (match find_positions env sigma t1 t2 with
@@ -445,24 +445,40 @@ let discr id gls =
 			([onLastHyp gen_absurdity;
 			  refine (mkApp (pf, [| mkVar id |]))]))) gls)
 
-
 let not_found_message id =
   (str "The variable" ++ spc () ++ str (string_of_id id) ++ spc () ++
     str" was not found in the current environment")
 
+let onEquality tac id gls =
+  let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in
+  let eq =
+    try find_eq_data_decompose eqn
+    with PatternMatchingFailure ->
+      errorlabstrm "" (pr_id id ++ str": not a primitive equality") 
+  in tac eq id gls
+
+let check_equality tac id gls =
+  let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in
+  let eq =
+    try find_eq_data_decompose eqn
+    with PatternMatchingFailure ->
+      errorlabstrm "" (str "The goal should negate an equality")
+  in tac eq id gls
+
 let onNegatedEquality tac gls =
-  if is_matching_not (pf_concl gls) then
-    (tclTHEN (tclTHEN hnf_in_concl intro) (onLastHyp tac)) gls
-  else if is_matching_imp_False (pf_concl gls)then
-    (tclTHEN intro (onLastHyp tac)) gls
-  else 
+   if is_matching_not (pf_concl gls) then
+     (tclTHEN (tclTHEN hnf_in_concl intro) (onLastHyp(check_equality tac))) gls
+   else if is_matching_imp_False (pf_concl gls)then
+     (tclTHEN intro (onLastHyp (check_equality tac))) gls
+  else
     errorlabstrm "extract_negated_equality_then"
       (str"The goal should negate an equality")
 
-
 let discrSimpleClause = function
-  | None -> onNegatedEquality discr
-  | Some (id,_,_) -> discr id
+  | None -> onNegatedEquality discrEq
+  | Some (id,_,_) -> onEquality discrEq id
+
+let discr = onEquality discrEq
 
 let discrClause = onClauses discrSimpleClause
 
@@ -566,7 +582,7 @@ let sig_clausal_form env sigma sort_of_ty siglen ty (dFLT,dFLTty) =
   let isevars = Evarutil.create_evar_defs sigma in
   let rec sigrec_clausal_form siglen p_i =
     if siglen = 0 then
-      if Evarconv.the_conv_x env isevars p_i dFLTty then
+      if Evarconv.the_conv_x_leq env isevars dFLTty p_i then
 	(* the_conv_x had a side-effect on isevars *)
 	dFLT
       else
@@ -695,13 +711,7 @@ let try_delta_expand env sigma t =
    expands then only when the whdnf has a constructor of an inductive type
    in hd position, otherwise delta expansion is not done *)
 
-let inj id gls =
-  let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in
-  let (eq,(t,t1,t2))= 
-    try find_eq_data_decompose eqn
-    with PatternMatchingFailure ->
-      errorlabstrm "Inj" (pr_id id ++ str": not a primitive equality here") 
-  in
+let injEq (eq,(t,t1,t2)) id gls =
   let sigma = project gls in
   let env = pf_env gls in
   match find_positions env sigma t1 t2 with
@@ -749,17 +759,17 @@ let inj id gls =
 	     in ((tclTHENS  (cut  ty) ([tclIDTAC;refine pf]))))
 	  injectors
 	  gls
-	    
+
+let inj = onEquality injEq
+
 let injClause = function
-  | None -> onNegatedEquality inj
+  | None -> onNegatedEquality injEq
   | Some id -> try_intros_until inj id
 
 let injConcl gls  = injClause None gls
 let injHyp id gls = injClause (Some id) gls
 
-let decompEqThen ntac id gls =
-  let eqn = pf_whd_betadeltaiota gls (pf_get_hyp_typ gls id) in
-  let (lbeq,(t,t1,t2))= find_eq_data_decompose eqn in
+let decompEqThen ntac (lbeq,(t,t1,t2)) id gls =
   let sort = pf_type_of gls (pf_concl gls) in 
   let sigma = project gls in
   let env = pf_env gls in 
@@ -806,17 +816,12 @@ let decompEqThen ntac id gls =
 	      (ntac (List.length injectors)))
 	  gls))
 
-let decompEq = decompEqThen (fun x -> tclIDTAC)
-
 let dEqThen ntac = function
   | None -> onNegatedEquality (decompEqThen ntac)
-  | Some id -> try_intros_until (decompEqThen ntac) id
+  | Some id -> try_intros_until (onEquality (decompEqThen ntac)) id
 
 let dEq = dEqThen (fun x -> tclIDTAC)
 
-let dEqConcl gls = dEq None gls
-let dEqHyp id gls = dEq (Some id) gls
-
 let rewrite_msg = function 
   | None -> str "passed term is not a primitive equality" 
   | Some id -> pr_id id ++ str "does not satisfy preconditions "
diff --git a/tactics/extraargs.mli b/tactics/extraargs.mli
index 60a1ddc5..2b4746ae 100644
--- a/tactics/extraargs.mli
+++ b/tactics/extraargs.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: extraargs.mli,v 1.3.2.1 2004/07/16 19:30:53 herbelin Exp $ *)
+(*i $Id: extraargs.mli,v 1.3.2.2 2005/01/21 17:14:10 herbelin Exp $ i*)
 
 open Tacexpr
 open Term
diff --git a/tactics/extratactics.ml4 b/tactics/extratactics.ml4
index 1dbf84ab..237f0a0d 100644
--- a/tactics/extratactics.ml4
+++ b/tactics/extratactics.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: extratactics.ml4,v 1.21.2.1 2004/07/16 19:30:53 herbelin Exp $ *)
+(* $Id: extratactics.ml4,v 1.21.2.2 2004/11/15 11:06:49 herbelin Exp $ *)
 
 open Pp
 open Pcoq
@@ -202,21 +202,21 @@ open Rawterm
 
 VERNAC COMMAND EXTEND DeriveInversion
 | [ "Derive" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ]
-  -> [ add_inversion_lemma_exn na c s false half_inv_tac ]
+  -> [ add_inversion_lemma_exn na c s false inv_tac ]
 
 | [ "Derive" "Inversion" ident(na) "with" constr(c) ]
-  -> [ add_inversion_lemma_exn na c (RProp Null) false half_inv_tac ]
+  -> [ add_inversion_lemma_exn na c (RProp Null) false inv_tac ]
 
 | [ "Derive" "Inversion" ident(na) hyp(id) ]
-  -> [ inversion_lemma_from_goal 1 na id Term.mk_Prop false half_inv_tac ]
+  -> [ inversion_lemma_from_goal 1 na id Term.mk_Prop false inv_tac ]
 
 | [ "Derive" "Inversion" natural(n) ident(na) hyp(id) ]
-  -> [ inversion_lemma_from_goal n na id Term.mk_Prop false half_inv_tac ]
+  -> [ inversion_lemma_from_goal n na id Term.mk_Prop false inv_tac ]
 END
 
 VERNAC COMMAND EXTEND DeriveDependentInversion
 | [ "Derive" "Dependent" "Inversion" ident(na) "with" constr(c) "Sort" sort(s) ]
-  -> [ add_inversion_lemma_exn na c s true half_dinv_tac ]
+  -> [ add_inversion_lemma_exn na c s true dinv_tac ]
     END
 
 VERNAC COMMAND EXTEND DeriveDependentInversionClear
diff --git a/tactics/extratactics.mli b/tactics/extratactics.mli
index a714c8dd..78a94190 100644
--- a/tactics/extratactics.mli
+++ b/tactics/extratactics.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: extratactics.mli,v 1.3.10.1 2004/07/16 19:30:53 herbelin Exp $ *)
+(*i $Id: extratactics.mli,v 1.3.10.2 2005/01/21 17:14:10 herbelin Exp $ i*)
 
 open Names
 open Term
diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli
index 816678ae..1b37291c 100644
--- a/tactics/hiddentac.mli
+++ b/tactics/hiddentac.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: hiddentac.mli,v 1.19.2.1 2004/07/16 19:30:53 herbelin Exp $ i*)
+(*i $Id: hiddentac.mli,v 1.19.2.2 2005/01/21 16:41:52 herbelin Exp $ i*)
 
 (*i*)
 open Names
@@ -78,9 +78,9 @@ val h_rename          : identifier -> identifier -> tactic
 
 
 (* Constructors *)
-(*
+(*i
 val h_any_constructor : tactic -> tactic
-*)
+i*)
 val h_constructor     : int -> constr bindings -> tactic
 val h_left            : constr bindings -> tactic
 val h_right           : constr bindings -> tactic
diff --git a/tactics/setoid_replace.mli b/tactics/setoid_replace.mli
index 565ae169..854fa478 100644
--- a/tactics/setoid_replace.mli
+++ b/tactics/setoid_replace.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: setoid_replace.mli,v 1.3.6.1 2004/07/16 19:30:55 herbelin Exp $ *)
+(*i $Id: setoid_replace.mli,v 1.3.6.2 2005/01/21 17:14:11 herbelin Exp $ i*)
 
 open Term
 open Proof_type
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 2080b5dc..4f8e7d7c 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.4 2004/07/16 19:30:55 herbelin Exp $ *)
+(* $Id: tacinterp.ml,v 1.84.2.8 2005/01/15 14:56:54 herbelin Exp $ *)
 
 open Constrintern
 open Closure
@@ -552,8 +552,7 @@ let intern_redexp ist = function
   | Lazy f -> Lazy (intern_flag ist f)
   | Pattern l -> Pattern (List.map (intern_constr_occurrence ist) l)
   | Simpl o -> Simpl (option_app (intern_constr_occurrence ist) o)
-  | (Red _ | Hnf as r) -> r
-  | ExtraRedExpr (s,c) -> ExtraRedExpr (s, intern_constr ist c)
+  | (Red _ | Hnf | ExtraRedExpr _ as r) -> r
 
 let intern_inversion_strength lf ist = function
   | NonDepInversion (k,idl,ids) ->
@@ -879,9 +878,12 @@ and intern_genarg ist x =
       in_gen globwit_red_expr (intern_redexp ist (out_gen rawwit_red_expr x))
   | TacticArgType ->
       in_gen globwit_tactic (intern_tactic ist (out_gen rawwit_tactic x))
+  | OpenConstrArgType ->
+      in_gen globwit_open_constr
+      ((),intern_constr ist (snd (out_gen rawwit_open_constr x)))
   | CastedOpenConstrArgType ->
       in_gen globwit_casted_open_constr 
-        (intern_constr ist (out_gen rawwit_casted_open_constr x))
+        ((),intern_constr ist (snd (out_gen rawwit_casted_open_constr x)))
   | ConstrWithBindingsArgType ->
       in_gen globwit_constr_with_bindings
         (intern_constr_with_bindings ist (out_gen rawwit_constr_with_bindings x))
@@ -964,6 +966,10 @@ let is_match_catchable = function
   | No_match | Eval_fail _ -> true
   | e -> is_failure e or Logic.catchable_exception e
 
+let hack_fail_level_shift = ref 0
+let hack_fail_level n =
+  if n >= !hack_fail_level_shift then n - !hack_fail_level_shift else 0
+
 (* Verifies if the matched list is coherent with respect to lcm *)
 let rec verify_metas_coherence gl lcm = function
   | (num,csr)::tl ->
@@ -1202,12 +1208,12 @@ let interp_constr ist sigma env c =
   interp_casted_constr None ist sigma env c
 
 (* Interprets an open constr expression casted by the current goal *)
-let pf_interp_casted_openconstr ist gl (c,ce) =
+let pf_interp_openconstr_gen casted ist gl (c,ce) =
   let sigma = project gl in
   let env = pf_env gl in
   let (ltacvars,l) = constr_list ist env in
   let typs = retype_list sigma env ltacvars in
-  let ocl = Some (pf_concl gl) in
+  let ocl = if casted then Some (pf_concl gl) else None in
   match ce with
   | None ->
       Pretyping.understand_gen_tcc sigma env typs ocl c
@@ -1216,6 +1222,9 @@ let pf_interp_casted_openconstr ist gl (c,ce) =
        intros/lettac/inversion hypothesis names *)
   | Some c -> interp_openconstr_gen sigma env (ltacvars,l) c ocl
 
+let pf_interp_casted_openconstr = pf_interp_openconstr_gen true
+let pf_interp_openconstr = pf_interp_openconstr_gen false
+
 (* Interprets a constr expression *)
 let pf_interp_constr ist gl =
   interp_constr ist (project gl) (pf_env gl)
@@ -1242,8 +1251,7 @@ let redexp_interp ist sigma env = function
   | Lazy f -> Lazy (interp_flag ist env f)
   | Pattern l -> Pattern (List.map (interp_pattern ist sigma env) l)
   | Simpl o -> Simpl (option_app (interp_pattern ist sigma env) o)
-  | (Red _ |  Hnf as r) -> r
-  | ExtraRedExpr (s,c) -> ExtraRedExpr (s,interp_constr ist sigma env c)
+  | (Red _ | Hnf | ExtraRedExpr _ as r) -> r
 
 let pf_redexp_interp ist gl = redexp_interp ist (project gl) (pf_env gl)
 
@@ -1349,7 +1357,7 @@ and eval_tactic ist = function
   | TacMatchContext _ -> assert false
   | TacMatch (c,lmr) -> assert false
   | TacId s -> tclIDTAC_MESSAGE s
-  | TacFail (n,s) -> tclFAIL (interp_int_or_var ist n) s
+  | TacFail (n,s) -> tclFAIL (hack_fail_level (interp_int_or_var ist n)) s
   | TacProgress tac -> tclPROGRESS (interp_tactic ist tac)
   | TacAbstract (tac,s) -> Tactics.tclABSTRACT s (interp_tactic ist tac)
   | TacThen (t1,t2) -> tclTHEN (interp_tactic ist t1) (interp_tactic ist t2)
@@ -1494,7 +1502,7 @@ and interp_match_context ist g lr lmr =
 	let lgoal = List.map (fun (id,c) -> (id,VConstr c)) lgoal in
         eval_with_fail { ist with lfun=lgoal@lctxt@ist.lfun } mt goal
       else
-        apply_hyps_context ist env goal mt lgoal mhyps hyps
+        apply_hyps_context ist env goal mt lctxt lgoal mhyps hyps
     with
     | e when is_failure e -> raise e
     | NextOccurrence _ -> raise No_match
@@ -1508,7 +1516,9 @@ and interp_match_context ist g lr lmr =
       begin
         db_mc_pattern_success ist.debug;
         try eval_with_fail ist t goal
-         with e when is_match_catchable e ->
+         with
+         | e when is_failure e -> raise e
+         | e when is_match_catchable e ->
            apply_match_context ist env goal (nrs+1) (List.tl lex) tl
       end
     | (Pat (mhyps,mgoal,mt))::tl ->
@@ -1529,9 +1539,10 @@ and interp_match_context ist g lr lmr =
               eval_with_fail {ist with lfun=lgoal@ist.lfun} mt goal
             end
             else
-              apply_hyps_context ist env goal mt lgoal mhyps hyps
+              apply_hyps_context ist env goal mt [] lgoal mhyps hyps
             end)
         with 
+        | e when is_failure e -> raise e
         | e when is_match_catchable e ->
           begin 
             (match e with
@@ -1542,7 +1553,9 @@ and interp_match_context ist g lr lmr =
           end)
       |	Subterm (id,mg) ->
         (try apply_goal_sub ist env goal 0 (id,mg) concl mt mhyps hyps
-         with e when is_match_catchable e ->
+         with 
+         | e when is_failure e -> raise e
+         | e when is_match_catchable e ->
            apply_match_context ist env goal (nrs+1) (List.tl lex) tl))
     | _ ->
       errorlabstrm "Tacinterp.apply_match_context" (str
@@ -1557,7 +1570,7 @@ and interp_match_context ist g lr lmr =
     (read_match_rule (project g) env (fst (constr_list ist env)) lmr)
 
 (* Tries to match the hypotheses in a Match Context *)
-and apply_hyps_context ist env goal mt lgmatch mhyps hyps =
+and apply_hyps_context ist env goal mt lctxt lgmatch mhyps hyps =
   let rec apply_hyps_context_rec lfun lmatch lhyps_rest current = function
     | Hyp ((_,hypname),mhyp)::tl as mhyps ->
         let (lids,lm,hyp_match,next) =
@@ -1578,7 +1591,7 @@ and apply_hyps_context ist env goal mt lgmatch mhyps hyps =
         db_mc_pattern_success ist.debug;
         eval_with_fail {ist with lfun=lmatch@lfun@ist.lfun} mt goal
   in
-  apply_hyps_context_rec [] lgmatch hyps (hyps,0) mhyps
+  apply_hyps_context_rec lctxt lgmatch hyps (hyps,0) mhyps
 
   (* Interprets extended tactic generic arguments *)
 and interp_genarg ist goal x =
@@ -1617,9 +1630,12 @@ and interp_genarg ist goal x =
   | RedExprArgType ->
       in_gen wit_red_expr (pf_redexp_interp ist goal (out_gen globwit_red_expr x))
   | TacticArgType -> in_gen wit_tactic (out_gen globwit_tactic x)
+  | OpenConstrArgType ->
+      in_gen wit_open_constr 
+        (pf_interp_openconstr ist goal (snd (out_gen globwit_open_constr x)))
   | CastedOpenConstrArgType ->
       in_gen wit_casted_open_constr 
-        (pf_interp_casted_openconstr ist goal (out_gen globwit_casted_open_constr x))
+        (pf_interp_casted_openconstr ist goal (snd (out_gen globwit_casted_open_constr x)))
   | ConstrWithBindingsArgType ->
       in_gen wit_constr_with_bindings
         (interp_constr_with_bindings ist goal (out_gen globwit_constr_with_bindings x))
@@ -1641,6 +1657,8 @@ and interp_match ist g constr lmr =
       let lm = List.map (fun (id,c) -> (id,VConstr c)) lm in
       val_interp {ist with lfun=lm@lctxt@ist.lfun} g mt
     with | NextOccurrence _ -> raise No_match
+         | e when is_match_catchable e -> 
+             apply_sub_match ist (nocc + 1) (id,c) csr mt
   in
   let rec apply_match ist csr = function
     | (All t)::_ ->
@@ -1668,7 +1686,14 @@ and interp_match ist g constr lmr =
       errorlabstrm "Tacinterp.apply_match" 
         (str "Argument of match does not evaluate to a term") in
   let ilr = read_match_rule (project g) env (fst (constr_list ist env)) lmr in
-  apply_match ist csr ilr
+  try
+    incr hack_fail_level_shift;
+    let x = apply_match ist csr ilr in
+    decr hack_fail_level_shift;
+    x
+  with e ->
+    decr hack_fail_level_shift;
+    raise e
 
 (* Interprets tactic expressions : returns a "tactic" *)
 and interp_tactic ist tac gl =
@@ -1829,7 +1854,7 @@ and interp_atomic ist gl = function
     | TacticArgType -> 
 	val_interp ist gl (out_gen globwit_tactic x)
     | StringArgType | BoolArgType
-    | QuantHypArgType | RedExprArgType 
+    | QuantHypArgType | RedExprArgType | OpenConstrArgType
     | CastedOpenConstrArgType | ConstrWithBindingsArgType | BindingsArgType 
     | ExtraArgType _ | List0ArgType _ | List1ArgType _ | OptArgType _ | PairArgType _ 
 	-> error "This generic type is not supported in alias"
@@ -1926,8 +1951,7 @@ let subst_redexp subst = function
   | Lazy f -> Lazy (subst_flag subst f)
   | Pattern l -> Pattern (List.map (subst_constr_occurrence subst) l)
   | Simpl o -> Simpl (option_app (subst_constr_occurrence subst) o)
-  | (Red _ | Hnf as r) -> r
-  | ExtraRedExpr (s,c) -> ExtraRedExpr (s, subst_rawconstr subst c)
+  | (Red _ | Hnf | ExtraRedExpr _ as r) -> r
 
 let subst_raw_may_eval subst = function
   | ConstrEval (r,c) -> ConstrEval (subst_redexp subst r,subst_rawconstr subst c)
@@ -2120,9 +2144,12 @@ and subst_genarg subst (x:glob_generic_argument) =
       in_gen globwit_red_expr (subst_redexp subst (out_gen globwit_red_expr x))
   | TacticArgType ->
       in_gen globwit_tactic (subst_tactic subst (out_gen globwit_tactic x))
+  | OpenConstrArgType ->
+      in_gen globwit_open_constr 
+        ((),subst_rawconstr subst (snd (out_gen globwit_open_constr x)))
   | CastedOpenConstrArgType ->
       in_gen globwit_casted_open_constr 
-        (subst_rawconstr subst (out_gen globwit_casted_open_constr x))
+        ((),subst_rawconstr subst (snd (out_gen globwit_casted_open_constr x)))
   | ConstrWithBindingsArgType ->
       in_gen globwit_constr_with_bindings
         (subst_raw_with_bindings subst (out_gen globwit_constr_with_bindings x))
diff --git a/tactics/tacticals.mli b/tactics/tacticals.mli
index 2cb63b40..111a5e2d 100644
--- a/tactics/tacticals.mli
+++ b/tactics/tacticals.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacticals.mli,v 1.38.2.1 2004/07/16 19:30:55 herbelin Exp $ i*)
+(*i $Id: tacticals.mli,v 1.38.2.2 2005/01/21 16:41:52 herbelin Exp $ i*)
 
 (*i*)
 open Names
@@ -127,7 +127,7 @@ type branch_assumptions = {
   ba        : branch_args;     (* the branch args *)
   assums    : named_context}   (* the list of assumptions introduced *)
 
-(* Useful for "as intro_pattern" modifier *)
+(* Useful for [as intro_pattern] modifier *)
 val compute_induction_names : 
   int -> intro_pattern_expr option -> intro_pattern_expr list array
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index cab4f025..b6eaf015 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.2 2004/07/16 19:30:55 herbelin Exp $ *)
+(* $Id: tactics.ml,v 1.162.2.4 2004/12/04 10:26:46 herbelin Exp $ *)
 
 open Pp
 open Util
@@ -654,7 +654,7 @@ let occurrences_of_hyp id cls =
 let occurrences_of_goal cls =
   if cls.onconcl then Some cls.concl_occs else None
 
-let everywhere cls = (cls=allClauses)
+let in_every_hyp cls = (cls.onhyps = None)
 
 (*
 (* Implementation with generalisation then re-intro: introduces noise *)
@@ -721,8 +721,8 @@ let letin_abstract id c occs gl =
       | None -> depdecls
       | Some occ ->
           let newdecl = subst_term_occ_decl occ c d in
-          if d = newdecl then
-	    if not (everywhere occs)
+          if occ = [] & d = newdecl then
+	    if not (in_every_hyp occs)
 	    then raise (RefinerError (DoesNotOccurIn (c,hyp)))
 	    else depdecls
           else 
@@ -1175,7 +1175,7 @@ let induct_discharge statuslists destopt avoid' ((avoid7,avoid8),ra) (names,forc
 		(match kind_of_term (pf_concl gl) with
 		  | Prod (name,t,_) -> (name,None,t)
 		  | LetIn (name,b,t,_) -> (name,Some b,t) 
-		  | _ -> assert false)) gl in
+		  | _ -> raise (RefinerError IntroNeedsProduct))) gl in
 	      if Options.do_translate() & id7 <> id8 then force := true;
               let id = if !Options.v7 then id7 else id8 in
 	      rnames := !rnames @ [IntroIdentifier id];
@@ -1192,12 +1192,12 @@ let induct_discharge statuslists destopt avoid' ((avoid7,avoid8),ra) (names,forc
 		(match kind_of_term (pf_concl gl) with
 		  | Prod (name,t,_) -> (name,None,t)
 		  | LetIn (name,b,t,_) -> (name,Some b,t) 
-		  | _ -> assert false)) gl in
+		  | _ -> raise (RefinerError IntroNeedsProduct))) gl in
 	      let id8 = fresh_id avoid8 (default_id gl
 		(match kind_of_term (pf_concl gl) with
 		  | Prod (name,t,_) -> (name,None,t)
 		  | LetIn (name,b,t,_) -> (name,Some b,t) 
-		  | _ -> assert false)) gl in
+		  | _ -> raise (RefinerError IntroNeedsProduct))) gl in
 	      if Options.do_translate() & id7 <> id8 then force := true;
               let id = if !Options.v7 then id7 else id8 in
               let avoid = if !Options.v7 then avoid7 else avoid8 in
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index 6e67a9cd..1155d845 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tactics.mli,v 1.59.2.1 2004/07/16 19:30:55 herbelin Exp $ i*)
+(*i $Id: tactics.mli,v 1.59.2.2 2005/01/21 16:41:52 herbelin Exp $ i*)
 
 (*i*)
 open Names
@@ -26,6 +26,7 @@ open Genarg
 open Tacexpr
 open Nametab
 open Rawterm
+(*i*)
 
 (* Main tactics. *)