Imported Upstream version 8.2~beta4+dfsgupstream/8.2.beta4+dfsg

8 files changed, 189 insertions, 199 deletions

diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 99ab7ef1..d19d81e0 100644
--- a/proofs/evar_refiner.ml
+++ b/proofs/evar_refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: evar_refiner.ml 11047 2008-06-03 23:08:00Z msozeau $ *)
+(* $Id: evar_refiner.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Util
 open Names
@@ -22,25 +22,28 @@ open Refiner
 
 (* w_tactic pour instantiate *) 
 
-let w_refine ev rawc evd =
-  if Evd.is_defined (evars_of evd) ev then 
+let w_refine evk rawc evd =
+  if Evd.is_defined (evars_of evd) evk then 
     error "Instantiate called on already-defined evar";
-  let e_info = Evd.find (evars_of evd) ev in
+  let e_info = Evd.find (evars_of evd) evk in
   let env = Evd.evar_env e_info in
-  let sigma,typed_c = 
+  let sigma,typed_c =
     try Pretyping.Default.understand_tcc ~resolve_classes:false
       (evars_of evd) env ~expected_type:e_info.evar_concl rawc
-    with _ -> error ("The term is not well-typed in the environment of " ^
-			string_of_existential ev)
+    with _ ->
+      let loc = Rawterm.loc_of_rawconstr rawc in
+      user_err_loc 
+        (loc,"",Pp.str ("Instance is not well-typed in the environment of " ^
+			string_of_existential evk))
   in
-    evar_define ev typed_c (evars_reset_evd sigma evd)
+    evar_define evk typed_c (evars_reset_evd sigma evd)
 
 (* vernac command Existential *)
 
 let instantiate_pf_com n com pfts = 
   let gls = top_goal_of_pftreestate pfts in
   let sigma = gls.sigma in 
-  let (sp,evi) (* as evc *) = 
+  let (evk,evi) = 
     let evl = Evarutil.non_instantiated sigma in
       if (n <= 0) then
 	error "incorrect existential variable index"
@@ -52,5 +55,5 @@ let instantiate_pf_com n com pfts =
   let env = Evd.evar_env evi in
   let rawc = Constrintern.intern_constr sigma env com in 
   let evd = create_goal_evar_defs sigma in
-  let evd' = w_refine sp rawc evd in
+  let evd' = w_refine evk rawc evd in
     change_constraints_pftreestate (evars_of evd') pfts
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 6e78f134..21ee9a9f 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: logic.ml 10877 2008-04-30 21:58:41Z herbelin $ *)
+(* $Id: logic.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -27,6 +27,7 @@ open Typeops
 open Type_errors
 open Retyping
 open Evarutil
+open Tacexpr
  
 type refiner_error =
 
@@ -47,13 +48,15 @@ open Pretype_errors
 
 let rec catchable_exception = function
   | Stdpp.Exc_located(_,e) -> catchable_exception e
+  | LtacLocated(_,e) -> catchable_exception e
   | Util.UserError _ | TypeError _ 
   | RefinerError _ | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _)
   (* unification errors *)
   | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
 		   |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
-		   |CannotFindWellTypedAbstraction _)) -> true
+		   |CannotFindWellTypedAbstraction _
+		   |UnsolvableImplicit _)) -> true
   | _ -> false
 
 (* Tells if the refiner should check that the submitted rules do not
@@ -70,11 +73,10 @@ let with_check = Flags.with_option check
    (instead of iterating on the list of identifier to be removed, which
    forces the user to give them in order). *)
 
-let clear_hyps sigma ids gl =
+let clear_hyps sigma ids sign cl =
   let evdref = ref (Evd.create_goal_evar_defs sigma) in
-  let (hyps,concl) =
-    Evarutil.clear_hyps_in_evi evdref gl.evar_hyps gl.evar_concl ids in
-    (mk_goal hyps concl gl.evar_extra, evars_of !evdref)
+  let (hyps,concl) = Evarutil.clear_hyps_in_evi evdref sign cl ids in
+  (hyps,concl,evars_of !evdref)
 
 (* The ClearBody tactic *)
 
@@ -83,13 +85,13 @@ let clear_hyps sigma ids gl =
 let apply_to_hyp sign id f =
   try apply_to_hyp sign id f 
   with Hyp_not_found -> 
-    if !check then error "No such assumption"
+    if !check then error "No such assumption."
     else sign
 
 let apply_to_hyp_and_dependent_on sign id f g =
   try apply_to_hyp_and_dependent_on sign id f g 
   with Hyp_not_found -> 
-    if !check then error "No such assumption"
+    if !check then error "No such assumption."
     else sign
 
 let check_typability env sigma c =
@@ -109,7 +111,7 @@ let remove_hyp_body env sigma id =
     apply_to_hyp_and_dependent_on (named_context_val env) id
       (fun (_,c,t) _ ->
 	match c with
-	| None -> error ((string_of_id id)^" is not a local definition")
+	| None -> error ((string_of_id id)^" is not a local definition.")
 	| Some c ->(id,None,t))
       (fun (id',c,t as d) sign ->
 	(if !check then
@@ -126,24 +128,42 @@ let remove_hyp_body env sigma id =
 
 (* Auxiliary functions for primitive MOVE tactic
  *
- * [move_after with_dep toleft (left,(hfrom,typfrom),right) hto] moves
- * hyp [hfrom] just after the hyp [hto] which belongs to the hyps on the 
+ * [move_hyp with_dep toleft (left,(hfrom,typfrom),right) hto] moves
+ * hyp [hfrom] at location [hto] which belongs to the hyps on the 
  * left side [left] of the full signature if [toleft=true] or to the hyps 
  * on the right side [right] if [toleft=false].
  * If [with_dep] then dependent hypotheses are moved accordingly. *)
 
+let error_no_such_hypothesis id =
+  error ("No such hypothesis: " ^ string_of_id id ^ ".")
+
+let rec get_hyp_after h = function
+  | [] -> error_no_such_hypothesis h
+  | (hyp,_,_) :: right ->
+      if hyp = h then
+	match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveToEnd false
+      else
+       get_hyp_after h right
+
 let split_sign hfrom hto l =
   let rec splitrec left toleft = function
-    | [] -> error ("No such hypothesis : " ^ (string_of_id hfrom))
+    | [] -> error_no_such_hypothesis hfrom
     | (hyp,c,typ) as d :: right ->
       	if hyp = hfrom then 
-	  (left,right,d,toleft) 
-      	else 
-	  splitrec (d::left) (toleft or (hyp = hto)) right
+	  (left,right,d, toleft or hto = MoveToEnd true)
+      	else
+	  splitrec (d::left) 
+	    (toleft or hto = MoveAfter hyp or hto = MoveBefore hyp)
+	    right
   in 
     splitrec [] false l
 
-let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
+let hyp_of_move_location = function
+  | MoveAfter id -> id 
+  | MoveBefore id -> id
+  | _ -> assert false
+
+let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
   let env = Global.env() in
   let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) =
     if toleft
@@ -151,23 +171,27 @@ let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
     else occur_var_in_decl env hyp d2
   in
   let rec moverec first middle = function
-    | [] -> error ("No such hypothesis : " ^ (string_of_id hto))
+    | [] ->
+	if match hto with MoveToEnd _ -> false | _ -> true then
+	  error_no_such_hypothesis (hyp_of_move_location hto);
+	List.rev first @ List.rev middle
+    | (hyp,_,_) :: _ as right when hto = MoveBefore hyp ->
+	List.rev first @ List.rev middle @ right
     | (hyp,_,_) as d :: right ->
 	let (first',middle') =
       	  if List.exists (test_dep d) middle then 
-	    if with_dep & (hyp <> hto) then 
+	    if with_dep & hto <> MoveAfter hyp then 
 	      (first, d::middle)
             else 
-	      error 
-		("Cannot move "^(string_of_id idfrom)^" after "
-		 ^(string_of_id hto)
-		 ^(if toleft then ": it occurs in " else ": it depends on ")
-		 ^(string_of_id hyp))
-          else 
+	      errorlabstrm "" (str "Cannot move " ++ pr_id idfrom ++
+	        pr_move_location pr_id hto ++ 
+	        str (if toleft then ": it occurs in " else ": it depends on ")
+	        ++ pr_id hyp ++ str ".")
+          else
 	    (d::first, middle)
 	in
-      	if hyp = hto then 
-	  (List.rev first')@(List.rev middle')@right
+      	if hto = MoveAfter hyp then
+	  List.rev first' @ List.rev middle' @ right
       	else 
 	  moverec first' middle' right
   in
@@ -183,53 +207,11 @@ let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
     List.fold_left (fun sign d -> push_named_context_val d sign)
       right left
 
-let check_backward_dependencies sign d =
-  if not (Idset.for_all
-	    (fun id -> mem_named_context id sign)
-	    (global_vars_set_of_decl (Global.env()) d))
-  then
-    error "Can't introduce at that location: free variable conflict"
-
-
-let check_forward_dependencies id tail =
-  let env = Global.env() in
-  List.iter
-    (function (id',_,_ as decl) ->
-       if occur_var_in_decl env id decl then
-	 error ((string_of_id id) ^ " is used in hypothesis " 
-		^ (string_of_id id')))
-    tail
-
-let check_goal_dependency id cl =
-  let env = Global.env() in
-    if Idset.mem id (global_vars_set env cl) then
-      error (string_of_id id^" is used in conclusion")
-
 let rename_hyp id1 id2 sign =
   apply_to_hyp_and_dependent_on sign id1
     (fun (_,b,t) _ -> (id2,b,t))
     (fun d _ -> map_named_declaration (replace_vars [id1,mkVar id2]) d)
 
-let replace_hyp sign id d cl =
-  if !check then
-    check_goal_dependency id cl;
-  apply_to_hyp sign id
-    (fun sign _ tail ->
-      if !check then
-	(check_backward_dependencies sign d;
-	 check_forward_dependencies id tail); 
-      d)
-
-(* why we dont check that id does not appear in tail ??? *)
-let insert_after_hyp sign id d =
-  try 
-    insert_after_hyp sign id d 
-      (fun sign ->
-	if !check then check_backward_dependencies sign d)
-  with Hyp_not_found ->
-    if !check then error "No such assumption"
-    else sign
-
 (************************************************************************)
 (************************************************************************)
 (* Implementation of the logical rules *)
@@ -375,19 +357,14 @@ and mk_casegoals sigma goal goalacc p c =
   (acc'',lbrty,conclty)
 
 
-let error_use_instantiate () =
-  errorlabstrm "Logic.prim_refiner"
-    (str"cannot intro when there are open metavars in the domain type" ++
-       spc () ++ str"- use Instantiate")
-
 let convert_hyp sign sigma (id,b,bt as d) =
   apply_to_hyp sign id
     (fun _ (_,c,ct) _ ->
        let env = Global.env_of_context sign in
        if !check && not (is_conv env sigma bt ct) then
-	 error ("Incorrect change of the type of "^(string_of_id id));
+	 error ("Incorrect change of the type of "^(string_of_id id)^".");
        if !check && not (Option.Misc.compare (is_conv env sigma) b c) then
-	 error ("Incorrect change of the body of "^(string_of_id id));
+	 error ("Incorrect change of the body of "^(string_of_id id)^".");
        d)
 
 (* Normalizing evars in a goal. Called by tactic Local_constraints
@@ -420,12 +397,10 @@ let prim_refiner r sigma goal =
 	  error "New variable is already declared";
         (match kind_of_term (strip_outer_cast cl) with
 	   | Prod (_,c1,b) ->
-	       if occur_meta c1 then error_use_instantiate();
 	       let sg = mk_goal (push_named_context_val (id,None,c1) sign)
 			  (subst1 (mkVar id) b) in
 	       ([sg], sigma)
 	   | LetIn (_,c1,t1,b) ->
-	       if occur_meta c1 or occur_meta t1 then error_use_instantiate();
 	       let sg =
 		 mk_goal (push_named_context_val (id,Some c1,t1) sign)
 		   (subst1 (mkVar id) b) in
@@ -433,28 +408,19 @@ let prim_refiner r sigma goal =
 	   | _ ->
 	       raise (RefinerError IntroNeedsProduct))
 	
-    | Intro_replacing id ->
-	(match kind_of_term (strip_outer_cast cl) with
-           | Prod (_,c1,b) ->
-	       if occur_meta c1 then error_use_instantiate();
-	       let sign' = replace_hyp sign id (id,None,c1) cl in
-	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
-	       ([sg], sigma)
-           | LetIn (_,c1,t1,b) ->
-	       if occur_meta c1 then error_use_instantiate();
-	       let sign' = replace_hyp sign id (id,Some c1,t1) cl in
-	       let sg = mk_goal sign' (subst1 (mkVar id) b) in
-	       ([sg], sigma)
-	   | _ ->
-	       raise (RefinerError IntroNeedsProduct))
-	
-    | Cut (b,id,t) ->
-    	if !check && mem_named_context id (named_context_of_val sign) then
-	  error "New variable is already declared";
-        if occur_meta t then error_use_instantiate();
+    | Cut (b,replace,id,t) ->
         let sg1 = mk_goal sign (nf_betaiota t) in
-        let sg2 = mk_goal (push_named_context_val (id,None,t) sign) cl in
-        if b then ([sg1;sg2],sigma) else ([sg2;sg1], sigma)
+	let sign,cl,sigma =
+	  if replace then
+	    let nexthyp = get_hyp_after id (named_context_of_val sign) in
+	    let sign,cl,sigma = clear_hyps sigma [id] sign cl in
+	    move_hyp true false ([],(id,None,t),named_context_of_val sign)
+	      nexthyp,
+	      cl,sigma
+	  else
+	    (push_named_context_val (id,None,t) sign),cl,sigma in
+        let sg2 = mk_goal sign cl in
+        if b then ([sg1;sg2],sigma) else ([sg2;sg1],sigma)
 
     | FixRule (f,n,rest) ->
      	let rec check_ind env k cl = 
@@ -464,10 +430,10 @@ let prim_refiner r sigma goal =
 		  try 
 		    fst (find_inductive env sigma c1)
 		  with Not_found -> 
-		    error "cannot do a fixpoint on a non inductive type"
+		    error "Cannot do a fixpoint on a non inductive type."
             	else 
 		  check_ind (push_rel (na,None,c1) env) (k-1) b
-            | _ -> error "not enough products"
+            | _ -> error "Not enough products."
 	in
 	let (sp,_) = check_ind env n cl in
 	let all = (f,n,cl)::rest in
@@ -475,10 +441,10 @@ let prim_refiner r sigma goal =
 	  | (f,n,ar)::oth ->
 	      let (sp',_)  = check_ind env n ar in 
 	      if not (sp=sp') then 
-		error ("fixpoints should be on the same " ^ 
-		       "mutual inductive declaration");
+		error ("Fixpoints should be on the same " ^ 
+		       "mutual inductive declaration.");
 	      if !check && mem_named_context f (named_context_of_val sign) then
-		error "name already used in the environment";
+		error "Name already used in the environment";
 	      mk_sign (push_named_context_val (f,None,ar) sign) oth
 	  | [] -> 
 	      List.map (fun (_,_,c) -> mk_goal sign c) all
@@ -495,8 +461,7 @@ let prim_refiner r sigma goal =
 		  let _ = find_coinductive env sigma b in ()
                 with Not_found -> 
 		  error ("All methods must construct elements " ^
-			  "in coinductiv-> goal
-e types")
+			  "in coinductive types.")
 	in
 	let all = (f,cl)::others in
      	List.iter (fun (_,c) -> check_is_coind env c) all;
@@ -504,7 +469,7 @@ e types")
           | (f,ar)::oth ->
 	      (try
                 (let _ = lookup_named_val f sign in
-                error "name already used in the environment")
+                error "Name already used in the environment.")
               with
               |	Not_found ->
                   mk_sign (push_named_context_val (f,None,ar) sign) oth)
@@ -533,8 +498,8 @@ e types")
 
     (* And now the structural rules *)
     | Thin ids -> 
-	let (ngl, nsigma) = clear_hyps sigma ids goal in
-	  ([ngl], nsigma)
+	let (hyps,concl,nsigma) = clear_hyps sigma ids sign cl in
+	  ([mk_goal hyps concl], nsigma)
 	
     | ThinBody ids ->
 	let clear_aux env id =
@@ -550,13 +515,13 @@ e types")
   	let (left,right,declfrom,toleft) = 
 	  split_sign hfrom hto (named_context_of_val sign) in
   	let hyps' = 
-	  move_after withdep toleft (left,declfrom,right) hto in
+	  move_hyp withdep toleft (left,declfrom,right) hto in
   	  ([mk_goal hyps' cl], sigma)
 
     | Rename (id1,id2) ->
         if !check & id1 <> id2 &&
 	  List.mem id2 (ids_of_named_context (named_context_of_val sign)) then
-          error ((string_of_id id2)^" is already used");
+          error ((string_of_id id2)^" is already used.");
         let sign' = rename_hyp id1 id2 sign in
         let cl' = replace_vars [id1,mkVar id2] cl in
           ([mk_goal sign' cl'], sigma)
@@ -617,20 +582,9 @@ let prim_extractor subfun vl pft =
 		let cb = subst_proof_vars vl b in
 		let cty = subst_proof_vars vl ty in
 		  mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
-	    | _ -> error "incomplete proof!")
+	    | _ -> error "Incomplete proof!")
 	    
-      | Some (Prim (Intro_replacing id),[spf]) ->
-	  (match kind_of_term (strip_outer_cast cl) with
-	    | Prod (_,ty,_) ->
-		let cty = subst_proof_vars vl ty in
-		  mkLambda (Name id, cty, subfun (add_proof_var id vl) spf)
-	    | LetIn (_,b,ty,_) ->
-		let cb = subst_proof_vars vl b in
-		let cty = subst_proof_vars vl ty in
-		  mkLetIn (Name id, cb, cty, subfun (add_proof_var id vl) spf)
-	    | _ -> error "incomplete proof!")
-
-      | Some (Prim (Cut (b,id,t)),[spf1;spf2]) ->
+      | Some (Prim (Cut (b,_,id,t)),[spf1;spf2]) ->
           let spf1, spf2 = if b then spf1, spf2 else spf2, spf1 in
 	    mkLetIn (Name id,subfun vl spf1,subst_proof_vars vl t,
                     subfun (add_proof_var id vl) spf2)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index dbe40780..41935c9c 100644
--- a/proofs/proof_type.ml
+++ b/proofs/proof_type.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: proof_type.ml 9842 2007-05-20 17:44:23Z herbelin $ *)
+(*i $Id: proof_type.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 (*i*)
 open Environ
@@ -28,8 +28,7 @@ open Pattern
 
 type prim_rule =
   | Intro of identifier
-  | Intro_replacing of identifier
-  | Cut of bool * identifier * types
+  | Cut of bool * bool * identifier * types
   | FixRule of identifier * int * (identifier * int * constr) list
   | Cofix of identifier * (identifier * constr) list
   | Refine of constr
@@ -37,7 +36,7 @@ type prim_rule =
   | Convert_hyp of named_declaration
   | Thin of identifier list
   | ThinBody of identifier list
-  | Move of bool * identifier * identifier
+  | Move of bool * identifier * identifier move_location
   | Rename of identifier * identifier
   | Change_evars
 
@@ -94,3 +93,16 @@ and tactic_arg =
 
 type hyp_location = identifier Tacexpr.raw_hyp_location
 
+type ltac_call_kind = 
+  | LtacNotationCall of string
+  | LtacNameCall of ltac_constant
+  | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref
+  | LtacVarCall of identifier * glob_tactic_expr
+  | LtacConstrInterp of rawconstr *
+      ((identifier * constr) list * (identifier * identifier option) list)
+
+type ltac_trace = (loc * ltac_call_kind) list
+
+exception LtacLocated of (ltac_call_kind * ltac_trace * loc) * exn
+
+let abstract_tactic_box = ref (ref None)
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 4fbcda4c..a7057a7d 100644
--- a/proofs/proof_type.mli
+++ b/proofs/proof_type.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: proof_type.mli 9842 2007-05-20 17:44:23Z herbelin $ i*)
+(*i $Id: proof_type.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
 
 (*i*)
 open Environ
@@ -28,8 +28,7 @@ open Pattern
 
 type prim_rule =
   | Intro of identifier
-  | Intro_replacing of identifier
-  | Cut of bool * identifier * types
+  | Cut of bool * bool * identifier * types
   | FixRule of identifier * int * (identifier * int * constr) list
   | Cofix of identifier * (identifier * constr) list
   | Refine of constr
@@ -37,7 +36,7 @@ type prim_rule =
   | Convert_hyp of named_declaration
   | Thin of identifier list
   | ThinBody of identifier list
-  | Move of bool * identifier * identifier
+  | Move of bool * identifier * identifier move_location
   | Rename of identifier * identifier
   | Change_evars
 
@@ -128,3 +127,17 @@ and tactic_arg =
      Tacexpr.gen_tactic_arg
 
 type hyp_location = identifier Tacexpr.raw_hyp_location
+
+type ltac_call_kind = 
+  | LtacNotationCall of string
+  | LtacNameCall of ltac_constant
+  | LtacAtomCall of glob_atomic_tactic_expr * atomic_tactic_expr option ref
+  | LtacVarCall of identifier * glob_tactic_expr
+  | LtacConstrInterp of rawconstr *
+      ((identifier * constr) list * (identifier * identifier option) list)
+
+type ltac_trace = (loc * ltac_call_kind) list
+
+exception LtacLocated of (ltac_call_kind * ltac_trace * loc) * exn
+
+val abstract_tactic_box : atomic_tactic_expr option ref ref
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 172a7d70..6e08e741 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: refiner.ml 11021 2008-05-29 16:48:18Z barras $ *)
+(* $Id: refiner.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -189,7 +189,6 @@ let leaf g =
 let check_subproof_connection gl spfl =
   list_for_all2eq (fun g pf -> Evd.eq_evar_info g pf.goal) gl spfl
 
-
 let abstract_operation syntax semantics gls =
   let (sgl_sigma,validation) = semantics gls in
   let hidden_proof = validation (List.map leaf sgl_sigma.it) in
@@ -204,6 +203,7 @@ let abstract_tactic_expr ?(dflt=false) te tacfun gls =
   abstract_operation (Tactic(te,dflt)) tacfun gls	
 
 let abstract_tactic ?(dflt=false) te =
+  !abstract_tactic_box := Some te;
   abstract_tactic_expr ~dflt (Tacexpr.TacAtom (dummy_loc,te))
 
 let abstract_extended_tactic ?(dflt=false) s args = 
@@ -491,13 +491,18 @@ let tclNOTSAMEGOAL (tac : tactic) goal =
       (str"Tactic generated a subgoal identical to the original goal.")
   else rslt
 
-let catch_failerror = function
-  | e when catchable_exception e -> check_for_interrupt ()
-  | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) ->
+let catch_failerror e =
+  if catchable_exception e then check_for_interrupt ()
+  else match e with
+  | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) 
+  | Stdpp.Exc_located(_, LtacLocated (_,FailError (0,_)))  ->
       check_for_interrupt ()
   | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
-  | Stdpp.Exc_located (s,FailError (lvl,s')) ->
-      raise (Stdpp.Exc_located (s,FailError (lvl - 1, s')))
+  | Stdpp.Exc_located(s,FailError (lvl,s')) ->
+      raise (Stdpp.Exc_located(s,FailError (lvl - 1, s')))
+  | Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl,s')))  ->
+      raise
+       (Stdpp.Exc_located(s,LtacLocated (s'',FailError (lvl - 1,s'))))
   | e -> raise e
 
 (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
@@ -548,14 +553,8 @@ let ite_gen tcal tac_if continue tac_else gl=
     try 
       tcal tac_if0 continue gl
     with (* Breakpoint *)
-      | e when catchable_exception e ->
-	  check_for_interrupt (); tac_else0 e gl
-      | (FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_))) as e ->
-	  check_for_interrupt (); tac_else0 e gl
-      | FailError (lvl,s) -> raise (FailError (lvl - 1, s))
-      | Stdpp.Exc_located (s,FailError (lvl,s')) ->
-	  raise (Stdpp.Exc_located (s,FailError (lvl - 1, s')))
-	
+      | e -> catch_failerror e; tac_else0 e gl
+
 (* Try the first tactic and, if it succeeds, continue with 
    the second one, and if it fails, use the third one *)
 
@@ -754,9 +753,7 @@ let extract_open_pftreestate pts =
 
 let extract_pftreestate pts =
   if pts.tstack <> [] then
-    errorlabstrm "extract_pftreestate"
-      (str"Cannot extract from a proof-tree in which we have descended;" ++
-         spc () ++ str"Please ascend to the root");
+    errorlabstrm "extract_pftreestate" (str"Proof blocks need to be closed");
   let pfterm,subgoals = extract_open_pftreestate pts in
   let exl = Evarutil.non_instantiated pts.tpfsigma in
   if subgoals <> [] or exl <> [] then
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index d0789980..8e51171f 100644
--- a/proofs/tacexpr.ml
+++ b/proofs/tacexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacexpr.ml 11100 2008-06-11 11:10:31Z herbelin $ i*)
+(*i $Id: tacexpr.ml 11309 2008-08-06 10:30:35Z herbelin $ i*)
 
 open Names
 open Topconstr
@@ -65,6 +65,20 @@ type hyp_location_flag = (* To distinguish body and type of local defs *)
 
 type 'a raw_hyp_location = 'a with_occurrences * hyp_location_flag
 
+type 'id move_location =
+  | MoveAfter of 'id
+  | MoveBefore of 'id
+  | MoveToEnd of bool
+
+let no_move = MoveToEnd true
+
+open Pp
+
+let pr_move_location pr_id = function
+  | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id
+  | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id
+  | MoveToEnd toleft -> str (if toleft then " at bottom" else " at top")
+
 type 'a induction_arg =
   | ElimOnConstr of 'a
   | ElimOnIdent of identifier located
@@ -76,8 +90,10 @@ type inversion_kind =
   | FullInversionClear
 
 type ('c,'id) inversion_strength =
-  | NonDepInversion of inversion_kind * 'id list * intro_pattern_expr
-  | DepInversion of inversion_kind * 'c option * intro_pattern_expr
+  | NonDepInversion of 
+      inversion_kind * 'id list * intro_pattern_expr located option
+  | DepInversion of
+      inversion_kind * 'c option * intro_pattern_expr located option
   | InversionUsing of 'c * 'id list
 
 type ('a,'b) location = HypLocation of 'a | ConclLocation of 'b
@@ -106,6 +122,11 @@ let simple_clause_of = function
 | _ ->
     error "not a simple clause (one hypothesis or conclusion)"
 
+type ('constr,'id) induction_clause = 
+    ('constr with_bindings induction_arg list * 'constr with_bindings option * 
+     (intro_pattern_expr located option * intro_pattern_expr located option) *
+     'id gclause option)
+
 type multi = 
   | Precisely of int
   | UpTo of int
@@ -130,14 +151,14 @@ type ('a,'t) match_rule =
 
 type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   (* Basic tactics *)
-  | TacIntroPattern of intro_pattern_expr list
+  | TacIntroPattern of intro_pattern_expr located list
   | TacIntrosUntil of quantified_hypothesis
-  | TacIntroMove of identifier option * identifier located option
+  | TacIntroMove of identifier option * 'id move_location
   | TacAssumption
   | TacExact of 'constr
   | TacExactNoCheck of 'constr
   | TacVmCastNoCheck of 'constr
-  | TacApply of advanced_flag * evars_flag * 'constr with_bindings
+  | TacApply of advanced_flag * evars_flag * 'constr with_bindings list
   | TacElim of evars_flag * 'constr with_bindings * 
       'constr with_bindings option
   | TacElimType of 'constr
@@ -149,19 +170,14 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacCofix of identifier option
   | TacMutualCofix of hidden_flag * identifier * (identifier * 'constr) list
   | TacCut of 'constr
-  | TacAssert of 'tac option * intro_pattern_expr * 'constr
+  | TacAssert of 'tac option * intro_pattern_expr located * 'constr
   | TacGeneralize of ('constr with_occurrences * name) list
   | TacGeneralizeDep of 'constr
   | TacLetTac of name * 'constr * 'id gclause * letin_flag
 
   (* Derived basic tactics *)
-  | TacSimpleInduction of quantified_hypothesis
-  | TacNewInduction of evars_flag * 'constr with_bindings induction_arg list * 
-      'constr with_bindings option * intro_pattern_expr * 'id gclause option
-  | TacSimpleDestruct of quantified_hypothesis
-  | TacNewDestruct of evars_flag * 'constr with_bindings induction_arg list *
-      'constr with_bindings option * intro_pattern_expr * 'id gclause option
-
+  | TacSimpleInductionDestruct of rec_flag * quantified_hypothesis
+  | TacInductionDestruct of rec_flag * evars_flag * ('constr,'id) induction_clause list
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
   | TacDecomposeAnd of 'constr
   | TacDecomposeOr of 'constr
@@ -181,7 +197,7 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   (* Context management *)
   | TacClear of bool * 'id list
   | TacClearBody of 'id list
-  | TacMove of bool * 'id * 'id
+  | TacMove of bool * 'id * 'id move_location
   | TacRename of ('id *'id) list
   | TacRevert of 'id list
 
@@ -236,7 +252,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
   | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
   | TacLetIn of rec_flag * (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
   | TacMatch of lazy_flag * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
-  | TacMatchContext of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
+  | TacMatchGoal of lazy_flag * direction_flag * ('pat,('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr) match_rule list
   | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast
   | TacArg of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg
 
@@ -249,7 +265,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg =
   | TacVoid
   | MetaIdArg      of loc * bool * string
   | ConstrMayEval  of ('constr,'cst) may_eval
-  | IntroPattern   of intro_pattern_expr
+  | IntroPattern   of intro_pattern_expr located
   | Reference      of 'ref
   | Integer        of int
   | TacCall        of loc *
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 213cc13f..6bbaff08 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,8 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacmach.ml 10544 2008-02-09 11:31:35Z herbelin $ *)
+(* $Id: tacmach.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
 
+open Pp
 open Util
 open Names
 open Nameops
@@ -58,7 +59,7 @@ let pf_get_hyp gls id =
   try 
     Sign.lookup_named id (pf_hyps gls)
   with Not_found -> 
-    error ("No such hypothesis : " ^ (string_of_id id))
+    error ("No such hypothesis: " ^ (string_of_id id))
 
 let pf_get_hyp_typ gls id =
   let (_,_,ty)= (pf_get_hyp gls id) in
@@ -175,15 +176,11 @@ let refiner = refiner
 let introduction_no_check id =
   refiner (Prim (Intro id))
 
-(* This does not check that the dependencies are correct *)
-let intro_replacing_no_check whereid gl = 
-  refiner (Prim (Intro_replacing whereid)) gl
-
-let internal_cut_no_check id t gl = 
-  refiner (Prim (Cut (true,id,t))) gl
+let internal_cut_no_check replace id t gl = 
+  refiner (Prim (Cut (true,replace,id,t))) gl
 
-let internal_cut_rev_no_check id t gl = 
-  refiner (Prim (Cut (false,id,t))) gl
+let internal_cut_rev_no_check replace id t gl = 
+  refiner (Prim (Cut (false,replace,id,t))) gl
 
 let refine_no_check c gl = 
   refiner (Prim (Refine c)) gl
@@ -220,13 +217,12 @@ let mutual_cofix f others gl =
 (* Versions with consistency checks *)
 
 let introduction id    = with_check (introduction_no_check id) 
-let intro_replacing id = with_check (intro_replacing_no_check id)
-let internal_cut d t     = with_check (internal_cut_no_check d t)
-let internal_cut_rev d t = with_check (internal_cut_rev_no_check d t)
+let internal_cut b d t = with_check (internal_cut_no_check b d t)
+let internal_cut_rev b d t = with_check (internal_cut_rev_no_check b d t)
 let refine c           = with_check (refine_no_check c)
 let convert_concl d sty = with_check (convert_concl_no_check d sty)
 let convert_hyp d      = with_check (convert_hyp_no_check d)
-let thin l             = with_check (thin_no_check l)
+let thin c             = with_check (thin_no_check c)
 let thin_body c        = with_check (thin_body_no_check c)
 let move_hyp b id id'  = with_check (move_hyp_no_check b id id') 
 let rename_hyp l       = with_check (rename_hyp_no_check l)
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 8b0053a4..2fc66e71 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tacmach.mli 11094 2008-06-10 19:35:23Z herbelin $ i*)
+(*i $Id: tacmach.mli 11309 2008-08-06 10:30:35Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -123,15 +123,15 @@ val change_constraints_pftreestate :
 
 val refiner                   : rule -> tactic
 val introduction_no_check     : identifier -> tactic
-val intro_replacing_no_check  : identifier -> tactic
-val internal_cut_no_check     : identifier -> types -> tactic
-val internal_cut_rev_no_check : identifier -> types -> tactic
+val internal_cut_no_check     : bool -> identifier -> types -> tactic
+val internal_cut_rev_no_check : bool -> identifier -> types -> tactic
 val refine_no_check           : constr -> tactic
 val convert_concl_no_check    : types -> cast_kind -> tactic
 val convert_hyp_no_check      : named_declaration -> tactic
 val thin_no_check             : identifier list -> tactic
 val thin_body_no_check        : identifier list -> tactic
-val move_hyp_no_check         : bool -> identifier -> identifier -> tactic
+val move_hyp_no_check         :
+  bool -> identifier -> identifier move_location -> tactic
 val rename_hyp_no_check       : (identifier*identifier) list -> tactic
 val mutual_fix      :
   identifier -> int -> (identifier * int * constr) list -> tactic
@@ -140,15 +140,14 @@ val mutual_cofix    : identifier -> (identifier * constr) list -> tactic
 (*s The most primitive tactics with consistency and type checking *)
 
 val introduction     : identifier -> tactic
-val intro_replacing  : identifier -> tactic
-val internal_cut     : identifier -> types -> tactic
-val internal_cut_rev : identifier -> types -> tactic
+val internal_cut     : bool -> identifier -> types -> tactic
+val internal_cut_rev : bool -> identifier -> types -> tactic
 val refine           : constr -> tactic
 val convert_concl    : types -> cast_kind -> tactic
 val convert_hyp      : named_declaration -> tactic
 val thin             : identifier list -> tactic
 val thin_body        : identifier list -> tactic
-val move_hyp         : bool -> identifier -> identifier -> tactic
+val move_hyp         : bool -> identifier -> identifier move_location -> tactic
 val rename_hyp       : (identifier*identifier) list -> tactic
 
 (*s Tactics handling a list of goals. *)