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

21 files changed, 414 insertions, 255 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 71538614..92794ac3 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: clenvtac.ml 8023 2006-02-10 18:34:51Z coq $ *)
+(* $Id: clenvtac.ml 11166 2008-06-22 13:23:35Z herbelin $ *)
 
 open Pp
 open Util
@@ -49,7 +49,7 @@ let clenv_cast_meta clenv =
     match kind_of_term (strip_outer_cast u) with
       | Meta mv ->
 	  (try 
-            let b = Typing.meta_type clenv.env mv in
+            let b = Typing.meta_type clenv.evd mv in
 	    if occur_meta b then u
             else mkCast (mkMeta mv, DEFAULTcast, b)
 	  with Not_found -> u)
@@ -60,25 +60,35 @@ let clenv_cast_meta clenv =
   in 
   crec
 
-let clenv_refine clenv gls =
+let clenv_value_cast_meta clenv =
+    clenv_cast_meta clenv (clenv_value clenv)
+
+let clenv_pose_dependent_evars with_evars clenv =
+  let dep_mvs = clenv_dependent false clenv in
+  if dep_mvs <> [] & not with_evars then
+    raise
+      (RefinerError (UnresolvedBindings (List.map (meta_name clenv.evd) dep_mvs)));
+  clenv_pose_metas_as_evars clenv dep_mvs
+
+
+let clenv_refine with_evars clenv gls =
+  let clenv = clenv_pose_dependent_evars with_evars clenv in
   tclTHEN
-    (tclEVARS (evars_of clenv.env)) 
+    (tclEVARS (evars_of clenv.evd)) 
     (refine (clenv_cast_meta clenv (clenv_value clenv)))
     gls
 
+let dft = Unification.default_unify_flags
 
-let res_pf clenv ?(allow_K=false) gls =
-  clenv_refine (clenv_unique_resolver allow_K clenv gls) gls
+let res_pf clenv ?(with_evars=false) ?(allow_K=false) ?(flags=dft) gls =
+  clenv_refine with_evars
+    (clenv_unique_resolver allow_K ~flags:flags clenv gls) gls
 
-let elim_res_pf_THEN_i clenv tac gls =  
+let elim_res_pf_THEN_i clenv tac gls =
   let clenv' = (clenv_unique_resolver true clenv gls) in
-  tclTHENLASTn (clenv_refine clenv') (tac clenv') gls
-
-
-let e_res_pf clenv gls =
-  clenv_refine (evar_clenv_unique_resolver clenv gls) gls
-
+  tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls
 
+let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft
 
 
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
@@ -86,11 +96,19 @@ let e_res_pf clenv gls =
    d'une même Meta sont compatibles. D'ailleurs le "fst" jette les metas
    provenant de w_Unify. (Utilisé seulement dans prolog.ml) *)
 
+open Unification
+
+let fail_quick_unif_flags = {
+  modulo_conv_on_closed_terms = Some full_transparent_state; 
+  use_metas_eagerly = false;
+  modulo_delta = empty_transparent_state;
+}
+
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
 let unifyTerms m n gls = 
   let env = pf_env gls in
-  let evd = create_evar_defs (project gls) in
-  let evd' = Unification.w_unify false env CONV m n evd in
+  let evd = create_goal_evar_defs (project gls) in
+  let evd' = w_unify false env CONV ~flags:fail_quick_unif_flags m n evd in
   tclIDTAC {it = gls.it; sigma = evars_of evd'}
 
 let unify m gls =
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 505826fa..29442ded 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: clenvtac.mli 6099 2004-09-12 11:38:09Z barras $ i*)
+(*i $Id: clenvtac.mli 11166 2008-06-22 13:23:35Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -16,11 +16,18 @@ open Sign
 open Evd
 open Clenv
 open Proof_type
+open Tacexpr
+open Unification
 (*i*)
 
 (* Tactics *)
 val unify : constr -> tactic
-val clenv_refine : clausenv -> tactic
-val res_pf : clausenv -> ?allow_K:bool -> tactic
-val e_res_pf : clausenv -> tactic
+val clenv_refine : evars_flag -> clausenv -> tactic
+val res_pf : clausenv -> ?with_evars:evars_flag -> ?allow_K:bool -> ?flags:unify_flags -> tactic
 val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic
+
+val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv
+val clenv_value_cast_meta : clausenv -> constr
+
+(* Compatibility, use res_pf ?with_evars:true instead *)
+val e_res_pf : clausenv -> tactic
diff --git a/proofs/decl_expr.mli b/proofs/decl_expr.mli
index a8b7c0d6..22752eda 100644
--- a/proofs/decl_expr.mli
+++ b/proofs/decl_expr.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: decl_expr.mli 10739 2008-04-01 14:45:20Z herbelin $ *)
 
 open Names
 open Util
@@ -18,7 +18,6 @@ type 'it statement =
 
 type thesis_kind =
     Plain
-  | Sub of int
   | For of identifier
 
 type 'this or_thesis =
diff --git a/proofs/decl_mode.ml b/proofs/decl_mode.ml
index 8d8fb745..f8fc4e87 100644
--- a/proofs/decl_mode.ml
+++ b/proofs/decl_mode.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(*i $Id: decl_mode.ml 10739 2008-04-01 14:45:20Z herbelin $ i*)
 
 open Names
 open Term
@@ -41,16 +41,19 @@ let check_not_proof_mode str =
    error str
 
 type split_tree=
-    Push of (Idset.t * split_tree)
-  | Split of (Idset.t * inductive * (Idset.t * split_tree) option array)
-  | Pop of split_tree
-  | End_of_branch of (identifier * int)
+    Skip_patt of Idset.t * split_tree
+  | Split_patt of Idset.t * inductive * 
+		(bool array * (Idset.t * split_tree) option) array
+  | Close_patt of split_tree
+  | End_patt of (identifier * int)
 
 type elim_kind =
     EK_dep of split_tree
   | EK_nodep
   | EK_unknown
 
+type recpath = int option*Declarations.wf_paths
+
 type per_info = 
     {per_casee:constr;
      per_ctype:types;
@@ -58,7 +61,8 @@ type per_info =
      per_pred:constr;
      per_args:constr list;
      per_params:constr list;
-     per_nparams:int}
+     per_nparams:int;
+     per_wf:recpath}
 
 type stack_info = 
     Per of Decl_expr.elim_type * per_info * elim_kind * identifier list
@@ -67,10 +71,7 @@ type stack_info =
   | Focus_claim
 
 type pm_info =
-    { pm_last: (Names.identifier * bool) option (* anonymous if none *);
-      pm_partial_goal : constr; (* partial goal construction *)
-      pm_subgoals : (metavariable*constr) list;
-      pm_stack : stack_info list}
+    { pm_stack : stack_info list}
 
 let pm_in,pm_out = Dyn.create "pm_info" 
 
@@ -118,3 +119,8 @@ let get_end_command pts =
 	end
     | Mode_none ->
         error "no proof in progress"
+
+let get_last env =  
+  try 
+    let (id,_,_) =  List.hd (Environ.named_context env) in id
+  with Invalid_argument _ -> error "no previous statement to use"
diff --git a/proofs/decl_mode.mli b/proofs/decl_mode.mli
index 81fab168..77bee313 100644
--- a/proofs/decl_mode.mli
+++ b/proofs/decl_mode.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id$ *)
+(* $Id: decl_mode.mli 10739 2008-04-01 14:45:20Z herbelin $ *)
 
 open Names
 open Term
@@ -29,16 +29,18 @@ val get_current_mode : unit -> command_mode
 val check_not_proof_mode : string -> unit
 
 type split_tree=
-    Push of  (Idset.t * split_tree)
-  | Split of (Idset.t * inductive * (Idset.t*split_tree) option array)
-  | Pop of split_tree
-  | End_of_branch of (identifier * int)
+    Skip_patt of Idset.t * split_tree
+  | Split_patt of Idset.t * inductive *
+		(bool array * (Idset.t * split_tree) option) array
+  | Close_patt of split_tree
+  | End_patt of (identifier * int)
 
 type elim_kind =
     EK_dep of split_tree
   | EK_nodep
   | EK_unknown
 
+type recpath = int option*Declarations.wf_paths
 
 type per_info = 
     {per_casee:constr;
@@ -47,7 +49,8 @@ type per_info =
      per_pred:constr;
      per_args:constr list;
      per_params:constr list;
-     per_nparams:int}
+     per_nparams:int;
+     per_wf:recpath}
 
 type stack_info = 
     Per of Decl_expr.elim_type * per_info * elim_kind * Names.identifier list
@@ -56,10 +59,7 @@ type stack_info =
   | Focus_claim
 
 type pm_info =
-    { pm_last: (Names.identifier * bool) option (* anonymous if none *);
-      pm_partial_goal : constr ; (* partial goal construction *)
-      pm_subgoals : (metavariable*constr) list;
-      pm_stack : stack_info list }
+    {pm_stack : stack_info list }
 
 val pm_in : pm_info -> Dyn.t
 
@@ -70,3 +70,5 @@ val get_end_command : pftreestate -> string option
 val get_stack : pftreestate -> stack_info list
 
 val get_top_stack : pftreestate -> stack_info list
+
+val get_last:  Environ.env -> identifier
diff --git a/proofs/evar_refiner.ml b/proofs/evar_refiner.ml
index 132fa2b9..99ab7ef1 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 9583 2007-02-01 19:35:03Z notin $ *)
+(* $Id: evar_refiner.ml 11047 2008-06-03 23:08:00Z msozeau $ *)
 
 open Util
 open Names
@@ -28,8 +28,8 @@ let w_refine ev rawc evd =
   let e_info = Evd.find (evars_of evd) ev in
   let env = Evd.evar_env e_info in
   let sigma,typed_c = 
-    try Pretyping.Default.understand_tcc (evars_of evd) env 
-      ~expected_type:e_info.evar_concl rawc 
+    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)
   in
@@ -41,12 +41,16 @@ 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 *) = 
-    try
-      List.nth (Evarutil.non_instantiated sigma) (n-1) 
-    with Failure _ -> 
-      error "not so many uninstantiated existential variables" in 
+    let evl = Evarutil.non_instantiated sigma in
+      if (n <= 0) then
+	error "incorrect existential variable index"
+      else if List.length evl < n then
+	  error "not so many uninstantiated existential variables"
+      else
+	List.nth evl (n-1)
+  in 
   let env = Evd.evar_env evi in
   let rawc = Constrintern.intern_constr sigma env com in 
-  let evd = create_evar_defs sigma in
+  let evd = create_goal_evar_defs sigma in
   let evd' = w_refine sp rawc evd in
-  change_constraints_pftreestate (evars_of evd') pfts
+    change_constraints_pftreestate (evars_of evd') pfts
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 0846997e..6e78f134 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: logic.ml 9805 2007-04-28 21:28:37Z herbelin $ *)
+(* $Id: logic.ml 10877 2008-04-30 21:58:41Z herbelin $ *)
 
 open Pp
 open Util
@@ -32,8 +32,7 @@ type refiner_error =
 
   (* Errors raised by the refiner *)
   | BadType of constr * constr * constr
-  | OccurMeta of constr
-  | OccurMetaGoal of constr
+  | UnresolvedBindings of name list
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
@@ -52,14 +51,15 @@ let rec catchable_exception = function
   | RefinerError _ | Indrec.RecursionSchemeError _
   | Nametab.GlobalizationError _ | PretypeError (_,VarNotFound _)
   (* unification errors *)
-  | PretypeError(_,(CannotUnify _|CannotGeneralize _|NoOccurrenceFound _|
-      CannotUnifyBindingType _|NotClean _)) -> true
+  | PretypeError(_,(CannotUnify _|CannotUnifyLocal _|CannotGeneralize _
+		   |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
+		   |CannotFindWellTypedAbstraction _)) -> true
   | _ -> false
 
 (* Tells if the refiner should check that the submitted rules do not
    produce invalid subgoals *)
 let check = ref false
-let with_check = Options.with_option check
+let with_check = Flags.with_option check
 
 (************************************************************************)
 (************************************************************************)
@@ -69,10 +69,12 @@ let with_check = Options.with_option check
 (* The Clear tactic: it scans the context for hypotheses to be removed
    (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 evd = ref (Evd.create_evar_defs sigma) in
-  let ngl = Evarutil.clear_hyps_in_evi evd gl ids in
-    (ngl, evars_of !evd)
+  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)
 
 (* The ClearBody tactic *)
 
@@ -264,8 +266,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 *)
   match kind_of_term trm with
     | Meta _ ->
-	if occur_meta conclty then
-          raise (RefinerError (OccurMetaGoal conclty));
+	if !check && occur_meta conclty then
+	  anomaly "refined called with a dependent meta";
 	(mk_goal hyps (nf_betaiota conclty))::goalacc, conclty
 
     | Cast (t,_, ty) ->
@@ -276,8 +278,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
     | App (f,l) ->
 	let (acc',hdty) =
 	  match kind_of_term f with
-	    | (Ind _ (* needed if defs in Type are polymorphic: | Const _*))
-		when not (array_exists occur_meta l) (* we could be finer *) ->
+	    | Ind _ | Const _
+		when not (array_exists occur_meta l) (* we could be finer *)
+		  & (isInd f or has_polymorphic_type (destConst f))
+		  ->
 		(* Sort-polymorphism of definition and inductive types *)
 		goalacc, 
 		type_of_global_reference_knowing_parameters env sigma f l
@@ -300,7 +304,8 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	(acc'',conclty')
 
     | _ -> 
-	if occur_meta trm then raise (RefinerError (OccurMeta trm));
+	if occur_meta trm then
+	  anomaly "refiner called with a meta in non app/case subterm";
       	let t'ty = goal_type_of env sigma trm in
 	check_conv_leq_goal env sigma trm t'ty conclty;
         (goalacc,t'ty)
@@ -340,7 +345,10 @@ and mk_hdgoals sigma goal goalacc trm =
 	in
 	(acc'',conclty')
 
-    | _ -> goalacc, goal_type_of env sigma trm
+    | _ ->
+	if !check && occur_meta trm then
+	  anomaly "refined called with a dependent meta";
+	goalacc, goal_type_of env sigma trm
 
 and mk_arggoals sigma goal goalacc funty = function
   | [] -> goalacc,funty
@@ -378,7 +386,7 @@ let convert_hyp sign sigma (id,b,bt as d) =
        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));
-       if !check && not (option_compare (is_conv env sigma) b c) then
+       if !check && not (Option.Misc.compare (is_conv env sigma) b c) then
 	 error ("Incorrect change of the body of "^(string_of_id id));
        d)
 
diff --git a/proofs/logic.mli b/proofs/logic.mli
index 2b6c6b4a..def02c8c 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: logic.mli 9573 2007-01-31 20:18:18Z notin $ i*)
+(*i $Id: logic.mli 10785 2008-04-13 21:41:54Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -50,8 +50,7 @@ type refiner_error =
 
   (*i Errors raised by the refiner i*)
   | BadType of constr * constr * constr
-  | OccurMeta of constr
-  | OccurMetaGoal of constr
+  | UnresolvedBindings of name list
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 565c9547..6d8f09ea 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pfedit.ml 9154 2006-09-20 17:18:18Z corbinea $ *)
+(* $Id: pfedit.ml 10850 2008-04-25 18:07:44Z herbelin $ *)
 
 open Pp
 open Util
@@ -33,6 +33,7 @@ open Safe_typing
 
 type proof_topstate = {
   mutable top_end_tac : tactic option;
+  top_init_tac : tactic option;
   top_goal : goal;
   top_strength : Decl_kinds.goal_kind;
   top_hook : declaration_hook }
@@ -118,8 +119,6 @@ let delete_proof (loc,id) =
     user_err_loc
       (loc,"Pfedit.delete_proof",str"No such proof" ++ msg_proofs false)
       
-let init_proofs () = Edit.clear proof_edits
-		       
 let mutate f =
   try 
     Edit.mutate proof_edits (fun _ pfs -> f pfs)
@@ -128,7 +127,8 @@ let mutate f =
       (str"No focused proof" ++ msg_proofs true)
 
 let start (na,ts) =
-  let pfs = mk_pftreestate ts.top_goal in 
+  let pfs = mk_pftreestate ts.top_goal in
+  let pfs = Option.fold_right solve_pftreestate ts.top_init_tac pfs in
   add_proof(na,pfs,ts)
     
 let restart_proof () =
@@ -204,13 +204,14 @@ let current_proof_depth() =
 let xml_cook_proof = ref (fun _ -> ())
 let set_xml_cook_proof f = xml_cook_proof := f
 
-let cook_proof () =
+let cook_proof k =
   let (pfs,ts) = get_state() 
   and ident = get_current_proof_name () in
   let {evar_concl=concl} = ts.top_goal 
   and strength = ts.top_strength in
   let pfterm = extract_pftreestate pfs in
   !xml_cook_proof (strength,pfs);
+  k pfs;
   (ident,
    ({ const_entry_body = pfterm;
       const_entry_type = Some concl;
@@ -237,7 +238,7 @@ let check_no_pending_proofs () =
 
 let delete_current_proof () = delete_proof_gen (get_current_proof_name ())
 
-let delete_all_proofs = init_proofs
+let delete_all_proofs () = Edit.clear proof_edits
 
 (*********************************************************************)
 (*   Modifying the end tactic of the current profftree               *)
@@ -250,10 +251,11 @@ let set_end_tac tac =
 (*              Modifying the current prooftree                      *)
 (*********************************************************************)
 
-let start_proof na str sign concl hook =
+let start_proof na str sign concl ?init_tac hook =
   let top_goal = mk_goal sign concl None in
   let ts = { 
     top_end_tac = None;
+    top_init_tac = init_tac;
     top_goal = top_goal;
     top_strength = str;
     top_hook = hook}
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 8c0c7f55..42c24081 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: pfedit.mli 9154 2006-09-20 17:18:18Z corbinea $ i*)
+(*i $Id: pfedit.mli 10850 2008-04-25 18:07:44Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -71,13 +71,16 @@ val current_proof_depth: unit -> int
 val set_undo : int option -> unit
 val get_undo : unit -> int option
 
-(*s [start_proof s str env t hook] starts a proof of name [s] and conclusion
-    [t]; [hook] is optionally a function to be applied at proof end (e.g. to
-    declare the built constructions as a coercion or a setoid morphism) *)
+(*s [start_proof s str env t hook tac] starts a proof of name [s] and
+    conclusion [t]; [hook] is optionally a function to be applied at
+    proof end (e.g. to declare the built constructions as a coercion
+    or a setoid morphism); init_tac is possibly a tactic to
+    systematically apply at initialization time (e.g. to start the
+    proof of mutually dependent theorems) *)
 
 val start_proof : 
-  identifier -> goal_kind -> named_context_val -> constr
-    -> declaration_hook -> unit
+  identifier -> goal_kind -> named_context_val -> constr ->
+    ?init_tac:tactic -> declaration_hook -> unit
 
 (* [restart_proof ()] restarts the current focused proof from the beginning
    or fails if no proof is focused *)
@@ -103,7 +106,7 @@ val suspend_proof : unit -> unit
     a constant with its name, kind and possible hook (see [start_proof]);
     it fails if there is no current proof of if it is not completed *)
 
-val cook_proof : unit -> 
+val cook_proof : (Refiner.pftreestate -> unit) -> 
   identifier * (Entries.definition_entry * goal_kind * declaration_hook)
 
 (* To export completed proofs to xml *)
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 9d70d012..99a1e506 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: proof_trees.ml 9154 2006-09-20 17:18:18Z corbinea $ *)
+(* $Id: proof_trees.ml 10124 2007-09-17 18:40:21Z herbelin $ *)
 
 open Closure
 open Util
@@ -35,6 +35,7 @@ let is_bind = function
 
 let mk_goal hyps cl extra = 
   { evar_hyps = hyps; evar_concl = cl; 
+    evar_filter = List.map (fun _ -> true) (named_context_of_val hyps);
     evar_body = Evar_empty; evar_extra = extra }
 
 (* Functions on proof trees *)
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 6f8b0686..dbe40780 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 9573 2007-01-31 20:18:18Z notin $ *)
+(*i $Id: proof_type.ml 9842 2007-05-20 17:44:23Z herbelin $ *)
 
 (*i*)
 open Environ
@@ -63,7 +63,7 @@ and tactic = goal sigma -> (goal list sigma * validation)
 and validation = (proof_tree list -> proof_tree)
 
 and tactic_expr =
-  (constr,
+  (open_constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
@@ -73,7 +73,7 @@ and tactic_expr =
      Tacexpr.gen_tactic_expr
 
 and atomic_tactic_expr =
-  (constr,
+  (open_constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
@@ -83,7 +83,7 @@ and atomic_tactic_expr =
      Tacexpr.gen_atomic_tactic_expr
 
 and tactic_arg =
-  (constr,
+  (open_constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index 26d9eb2e..4fbcda4c 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 9573 2007-01-31 20:18:18Z notin $ i*)
+(*i $Id: proof_type.mli 9842 2007-05-20 17:44:23Z herbelin $ i*)
 
 (*i*)
 open Environ
@@ -98,7 +98,7 @@ and tactic = goal sigma -> (goal list sigma * validation)
 and validation = (proof_tree list -> proof_tree)
 
 and tactic_expr =
-  (constr,
+  (open_constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
@@ -108,7 +108,7 @@ and tactic_expr =
      Tacexpr.gen_tactic_expr
 
 and atomic_tactic_expr =
-  (constr,
+  (open_constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
@@ -118,7 +118,7 @@ and atomic_tactic_expr =
      Tacexpr.gen_atomic_tactic_expr
 
 and tactic_arg =
-  (constr,
+  (open_constr,
    constr_pattern,
    evaluable_global_reference,
    inductive,
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index ad277caa..072a38b6 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: redexpr.ml 9058 2006-07-22 17:42:45Z bgregoir $ *)
+(* $Id: redexpr.ml 11094 2008-06-10 19:35:23Z herbelin $ *)
 
 open Pp
 open Util
@@ -19,7 +19,7 @@ open Reductionops
 open Tacred
 open Closure
 open RedFlags
-
+open Libobject
 
 (* call by value normalisation function using the virtual machine *)
 let cbv_vm env _ c =
@@ -27,22 +27,79 @@ let cbv_vm env _ c =
   Vnorm.cbv_vm env c ctyp
 
 
-let set_opaque_const sp = 
-  Conv_oracle.set_opaque_const sp;
-  Csymtable.set_opaque_const sp
-
-let set_transparent_const sp =
-  let cb = Global.lookup_constant sp in
-  if cb.const_body <> None & cb.const_opaque then
-    errorlabstrm "set_transparent_const"
-      (str "Cannot make" ++ spc () ++ 
-         Nametab.pr_global_env Idset.empty (ConstRef sp) ++
-         spc () ++ str "transparent because it was declared opaque.");
-  Conv_oracle.set_transparent_const sp;
-  Csymtable.set_transparent_const sp
-
-let set_opaque_var      = Conv_oracle.set_opaque_var
-let set_transparent_var = Conv_oracle.set_transparent_var
+let set_strategy_one ref l  =
+  let k =
+    match ref with
+      | EvalConstRef sp -> ConstKey sp
+      | EvalVarRef id -> VarKey id in
+  Conv_oracle.set_strategy k l;
+  match k,l with
+      ConstKey sp, Conv_oracle.Opaque ->
+        Csymtable.set_opaque_const sp
+    | ConstKey sp, _ ->
+        let cb = Global.lookup_constant sp in
+        if cb.const_body <> None & cb.const_opaque then
+          errorlabstrm "set_transparent_const"
+            (str "Cannot make" ++ spc () ++ 
+            Nametab.pr_global_env Idset.empty (ConstRef sp) ++
+            spc () ++ str "transparent because it was declared opaque.");
+        Csymtable.set_transparent_const sp
+    | _ -> ()
+
+let cache_strategy str =
+  List.iter 
+    (fun (lev,ql) -> List.iter (fun q -> set_strategy_one q lev) ql)
+    str
+
+let subst_strategy (_,subs,obj) =
+  list_smartmap
+    (fun (k,ql as entry) ->
+      let ql' = list_smartmap (Mod_subst.subst_evaluable_reference subs) ql in
+      if ql==ql' then entry else (k,ql'))
+    obj
+
+
+let map_strategy f l =
+  let l'  = List.fold_right
+    (fun (lev,ql) str -> 
+      let ql' = List.fold_right
+        (fun q ql ->
+          match f q with
+              Some q' -> q' :: ql
+            | None -> ql) ql [] in
+      if ql'=[] then str else (lev,ql')::str) l [] in
+  if l'=[] then None else Some l'
+
+let export_strategy obj =
+  map_strategy (function
+      EvalVarRef _ -> None
+    | EvalConstRef _ as q -> Some q) obj
+
+let classify_strategy (_,obj) = Substitute obj
+
+let disch_ref ref =
+  match ref with
+      EvalConstRef c -> 
+        let c' = Lib.discharge_con c in
+        if c==c' then Some ref else Some (EvalConstRef c')
+    | _ -> Some ref
+
+let discharge_strategy (_,obj) =
+  map_strategy disch_ref obj
+
+let (inStrategy,outStrategy) =
+  declare_object {(default_object "STRATEGY") with
+                    cache_function = (fun (_,obj) -> cache_strategy obj);
+		    load_function = (fun _ (_,obj) -> cache_strategy obj);
+		    subst_function = subst_strategy;
+                    discharge_function = discharge_strategy;
+		    classify_function = classify_strategy;
+                    export_function = export_strategy }
+
+
+let set_strategy local str =
+  if local then cache_strategy str
+  else Lib.add_anonymous_leaf (inStrategy str)
 
 let _ = 
   Summary.declare_summary "Transparent constants and variables"
@@ -70,7 +127,7 @@ let make_flag f =
   let red =
     if f.rDelta then (* All but rConst *)
         let red = red_add red fDELTA in
-        let red = red_add_transparent red (Conv_oracle.freeze ()) in
+        let red = red_add_transparent red (Conv_oracle.get_transp_state()) in
 	List.fold_right
 	  (fun v red -> red_sub red (make_flag_constant v))
 	  f.rConst red
@@ -97,8 +154,8 @@ let out_arg = function
   | ArgVar _ -> anomaly "Unevaluated or_var variable"
   | ArgArg x -> x
 
-let out_with_occurrences (l,c) =
-  (List.map out_arg l, c)
+let out_with_occurrences ((b,l),c) =
+  ((b,List.map out_arg l), c)
 
 let reduction_of_red_expr = function
   | Red internal -> 
@@ -106,8 +163,8 @@ let reduction_of_red_expr = function
       else (red_product,DEFAULTcast)
   | Hnf -> (hnf_constr,DEFAULTcast)
   | Simpl (Some (_,c as lp)) ->
-      (contextually (is_reference c) (out_with_occurrences lp) nf,DEFAULTcast)
-  | Simpl None -> (nf,DEFAULTcast)
+    (contextually (is_reference c) (out_with_occurrences lp) simpl,DEFAULTcast)
+  | Simpl None -> (simpl,DEFAULTcast)
   | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast)
   | Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast)
   | Unfold ubinds -> (unfoldn (List.map out_with_occurrences ubinds),DEFAULTcast)
diff --git a/proofs/redexpr.mli b/proofs/redexpr.mli
index cbac180a..d72ff182 100644
--- a/proofs/redexpr.mli
+++ b/proofs/redexpr.mli
@@ -6,18 +6,19 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: redexpr.mli 8878 2006-05-30 16:44:25Z herbelin $ i*)
+(*i $Id: redexpr.mli 11094 2008-06-10 19:35:23Z herbelin $ i*)
 
 open Names
 open Term
 open Closure
 open Rawterm
 open Reductionops
+open Termops
 
 
 type red_expr = (constr, evaluable_global_reference) red_expr_gen
 
-val out_with_occurrences : 'a with_occurrences -> int list * 'a
+val out_with_occurrences : 'a with_occurrences -> occurrences * 'a
 
 val reduction_of_red_expr : red_expr -> reduction_function * cast_kind
 (* [true] if we should use the vm to verify the reduction *)
@@ -25,13 +26,12 @@ val reduction_of_red_expr : red_expr -> reduction_function * cast_kind
 val declare_red_expr : string -> reduction_function -> unit
 
 (* Opaque and Transparent commands. *)
-val set_opaque_const      : constant -> unit
-val set_transparent_const : constant -> unit
-
-val set_opaque_var      : identifier -> unit
-val set_transparent_var : identifier -> unit
-
 
+(* Sets the expansion strategy of a constant. When the boolean is
+   true, the effect is non-synchronous (i.e. it does not survive
+   section and module closure). *)
+val set_strategy :
+  bool -> (Conv_oracle.level * evaluable_global_reference list) list -> unit
 
 (* call by value normalisation function using the virtual machine *)
 val cbv_vm : reduction_function
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index a1d7e011..172a7d70 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: refiner.ml 9573 2007-01-31 20:18:18Z notin $ *)
+(* $Id: refiner.ml 11021 2008-05-29 16:48:18Z barras $ *)
 
 open Pp
 open Util
@@ -108,13 +108,23 @@ let rec frontier p =
 		  open_subgoals = and_status (List.map pf_status pfl');
 		  ref = Some(r,pfl')}))
 
+(* TODO LEM: I might have to make sure that these hooks are called
+   only when called from solve_nth_pftreestate; I can build the hook
+   call into the "f", then.
+ *)
+let solve_hook = ref ignore
+let set_solve_hook = (:=) solve_hook
 
 let rec frontier_map_rec f n p =
   if n < 1 || n > p.open_subgoals then p else
   match p.ref with
     | None -> 
         let p' = f p in
-        if Evd.eq_evar_info p'.goal p.goal then p'
+        if Evd.eq_evar_info p'.goal p.goal then
+	  begin
+	    !solve_hook p';
+	    p'
+	  end
         else 
 	  errorlabstrm "Refiner.frontier_map"
             (str"frontier_map was handed back a ill-formed proof.")
@@ -140,7 +150,11 @@ let rec frontier_mapi_rec f i p =
   match p.ref with
     | None -> 
         let p' = f i p in
-        if Evd.eq_evar_info p'.goal p.goal then p'
+        if Evd.eq_evar_info p'.goal p.goal then
+	  begin
+	    !solve_hook p';
+	    p'
+	  end
         else 
 	  errorlabstrm "Refiner.frontier_mapi"
             (str"frontier_mapi was handed back a ill-formed proof.")
@@ -223,9 +237,7 @@ let refiner = function
              ref = Some(Daimon,[])})
 
 
-let local_Constraints gl = refiner (Prim Change_evars) gl
-
-let norm_evar_tac = local_Constraints
+let norm_evar_tac gl = refiner (Prim Change_evars) gl
 
 let norm_evar_proof sigma pf =
   let nf_subgoal i sgl =
@@ -312,6 +324,9 @@ let idtac_valid = function
 (* [goal_goal_list : goal sigma -> goal list sigma] *)
 let goal_goal_list gls = {it=[gls.it];sigma=gls.sigma}
 
+(* forces propagation of evar constraints *)
+let tclNORMEVAR = norm_evar_tac
+
 (* identity tactic without any message *)
 let tclIDTAC gls = (goal_goal_list gls, idtac_valid)
 
@@ -334,29 +349,25 @@ let start_tac gls =
 
 let finish_tac (sigr,gl,p) = (repackage sigr gl, p)
 
-(* Apply [taci.(i)] on the first n-th subgoals and [tac] on the others *)
-let thensf_tac taci tac (sigr,gs,p) =
-  let n = Array.length taci in
-  let nsg = List.length gs in
-  if nsg<n then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
+(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
+let thens3parts_tac tacfi tac tacli (sigr,gs,p) =
+  let nf = Array.length tacfi in
+  let nl = Array.length tacli in
+  let ng = List.length gs in
+  if ng<nf+nl then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
   let gll,pl =
     List.split
-      (list_map_i (fun i -> apply_sig_tac sigr (if i<n then taci.(i) else tac))
+      (list_map_i (fun i -> 
+        apply_sig_tac sigr (if i<nf then tacfi.(i) else if i>=ng-nl then tacli.(nl-ng+i) else tac))
 	0 gs) in
   (sigr, List.flatten gll,
    compose p (mapshape (List.map List.length gll) pl))
 
-(* Apply [taci.(i)] on the last n-th subgoals and [tac] on the others *)
-let thensl_tac tac taci (sigr,gs,p) =
-  let n = Array.length taci in
-  let nsg = List.length gs in
-  if nsg<n then errorlabstrm "Refiner.thensn_tac" (str "Not enough subgoals.");
-  let gll,pl =
-    List.split
-      (list_map_i (fun i -> apply_sig_tac sigr (if i<0 then tac else taci.(i)))
-	(n-nsg) gs) in
-  (sigr, List.flatten gll,
-   compose p (mapshape (List.map List.length gll) pl))
+(* Apply [taci.(i)] on the first n subgoals and [tac] on the others *)
+let thensf_tac taci tac = thens3parts_tac taci tac [||]
+
+(* Apply [taci.(i)] on the last n subgoals and [tac] on the others *)
+let thensl_tac tac taci = thens3parts_tac [||] tac taci
 
 (* Apply [tac i] on the ith subgoal (no subgoals number check) *)
 let thensi_tac tac (sigr,gs,p) =
@@ -382,19 +393,25 @@ let theni_tac i tac ((_,gl,_) as subgoals) =
       subgoals
   else non_existent_goal k 
 
+(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
+   applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
+   the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
+   subgoals and [tac2] to the rest of the subgoals in the middle. Raises an
+   error if the number of resulting subgoals is strictly less than [n+m] *)
+let tclTHENS3PARTS tac1 tacfi tac tacli gls =
+  finish_tac (thens3parts_tac tacfi tac tacli (then_tac tac1 (start_tac gls)))
+
 (* [tclTHENSFIRSTn tac1 [|t1 ; ... ; tn|] tac2 gls] applies the tactic [tac1]
-   to [gls] and applies [t1], ..., [tn] to the [n] first resulting
+   to [gls] and applies [t1], ..., [tn] to the first [n] resulting
    subgoals, and [tac2] to the others subgoals. Raises an error if
    the number of resulting subgoals is strictly less than [n] *)
-let tclTHENSFIRSTn tac1 taci tac gls =
-  finish_tac (thensf_tac taci tac (then_tac tac1 (start_tac gls)))
+let tclTHENSFIRSTn tac1 taci tac = tclTHENS3PARTS tac1 taci tac [||]
 
 (* [tclTHENSLASTn tac1 tac2 [|t1 ;...; tn|] gls] applies the tactic [tac1]
-   to [gls] and applies [t1], ..., [tn] to the [n] last resulting
+   to [gls] and applies [t1], ..., [tn] to the last [n] resulting
    subgoals, and [tac2] to the other subgoals. Raises an error if the
    number of resulting subgoals is strictly less than [n] *)
-let tclTHENSLASTn tac1 tac taci gls =
-  finish_tac (thensl_tac tac taci (then_tac tac1 (start_tac gls)))
+let tclTHENSLASTn tac1 tac taci = tclTHENS3PARTS tac1 [||] tac taci
 
 (* [tclTHEN_i tac taci gls] applies the tactic [tac] to [gls] and applies
    [(taci i)] to the i_th resulting subgoal (starting from 1), whatever the
@@ -407,13 +424,13 @@ let tclTHENFIRSTn tac1 taci = tclTHENSFIRSTn tac1 taci tclIDTAC
 
 (* [tclTHEN tac1 tac2 gls] applies the tactic [tac1] to [gls] and applies
    [tac2] to every resulting subgoals *)
-let tclTHEN tac1 tac2 = tclTHENSFIRSTn tac1 [||] tac2
+let tclTHEN tac1 tac2 = tclTHENS3PARTS tac1 [||] tac2 [||]
 
 (* [tclTHENSV tac1 [t1 ; ... ; tn] gls] applies the tactic [tac1] to
    [gls] and applies [t1],..., [tn] to the [n] resulting subgoals. Raises
    an error if the number of resulting subgoals is not [n] *)
 let tclTHENSV tac1 tac2v =
-  tclTHENSFIRSTn tac1 tac2v (tclFAIL_s "Wrong number of tactics.")
+  tclTHENS3PARTS tac1 tac2v (tclFAIL_s "Wrong number of tactics.") [||]
 
 let tclTHENS tac1 tac2l = tclTHENSV tac1 (Array.of_list tac2l)
 
@@ -425,7 +442,6 @@ let tclTHENLAST tac1 tac2 = tclTHENSLASTn tac1 tclIDTAC [|tac2|]
    to the first resulting subgoal *)
 let tclTHENFIRST tac1 tac2 = tclTHENSFIRSTn tac1 [|tac2|] tclIDTAC
 
-
 (* [tclTHENLIST [t1;..;tn]] applies [t1] then [t2] ... then [tn]. More
    convenient than [tclTHEN] when [n] is large. *)
 let rec tclTHENLIST = function
@@ -437,18 +453,17 @@ let rec tclTHENLIST = function
 
 (* various progress criterions *)
 let same_goal gl subgoal = 
-  eq_named_context_val (hypotheses subgoal) (hypotheses gl) &&
-  eq_constr (conclusion subgoal) (conclusion gl)
+  eq_constr (conclusion subgoal) (conclusion gl) &&
+  eq_named_context_val (hypotheses subgoal) (hypotheses gl)
 
 
 let weak_progress gls ptree =
-  (List.length gls.it <> 1) or 
+  (List.length gls.it <> 1) || 
   (not (same_goal (List.hd gls.it) ptree.it))
 
-(* Il y avait ici un ts_eq ........ *)
 let progress gls ptree =
-  (weak_progress gls ptree) or
-  (not (ptree.sigma == gls.sigma))
+  (not (ptree.sigma == gls.sigma)) ||
+  (weak_progress gls ptree)
 
 
 (* PROGRESS tac ptree applies tac to the goal ptree and fails if tac leaves
@@ -476,24 +491,39 @@ 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,_)) ->
+      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')))
+  | e -> raise e
 
 (* ORELSE0 t1 t2 tries to apply t1 and if it fails, applies t2 *)
 let tclORELSE0 t1 t2 g =
   try 
     t1 g
   with (* Breakpoint *)
-  | e when catchable_exception e -> check_for_interrupt (); t2 g
-  | FailError (0,_) | Stdpp.Exc_located(_, FailError (0,_)) ->
-      check_for_interrupt (); t2 g
-  | 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; t2 g
 
 (* ORELSE t1 t2 tries to apply t1 and if it fails or does not progress, 
    then applies t2 *)
 let tclORELSE t1 t2 = tclORELSE0 (tclPROGRESS t1) t2
 
+(* applies t1;t2then if t1 succeeds or t2else if t1 fails
+   t2* are called in terminal position (unless t1 produces more than
+   1 subgoal!) *) 
+let tclORELSE_THEN t1 t2then t2else gls =
+  match
+    try Some(tclPROGRESS t1 gls)
+    with e -> catch_failerror e; None
+  with
+    | None -> t2else gls
+    | Some (sgl,v) ->
+        let (sigr,gl) = unpackage sgl in 
+        finish_tac (then_tac t2then  (sigr,gl,v))
+
 (* TRY f tries to apply f, and if it fails, leave the goal unchanged *)
 let tclTRY f = (tclORELSE0 f tclIDTAC)
 
@@ -558,9 +588,10 @@ let tclDO n t =
   in 
   dorec n 
 
+
 (* Beware: call by need of CAML, g is needed *)
 let rec tclREPEAT t g =
-  (tclORELSE (tclTHEN t (tclREPEAT t)) tclIDTAC) g
+  tclORELSE_THEN t (tclREPEAT t) tclIDTAC g
 
 let tclAT_LEAST_ONCE t = (tclTHEN t (tclREPEAT t))
 
@@ -847,6 +878,7 @@ let prev_unproven pts =
 let rec top_of_tree pts = 
   if is_top_pftreestate pts then pts else top_of_tree(traverse 0 pts)
 
+(* FIXME: cette fonction n'est (as of October 2007) appelée nulle part *)
 let change_rule f pts =
   let mark_top _ pt =
     match pt.ref with
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index d8b13dba..95130ac5 100644
--- a/proofs/refiner.mli
+++ b/proofs/refiner.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: refiner.mli 9244 2006-10-16 17:11:44Z barras $ i*)
+(*i $Id: refiner.mli 10879 2008-05-01 22:14:20Z msozeau $ i*)
 
 (*i*)
 open Term
@@ -28,7 +28,7 @@ val pf_hyps : goal sigma -> named_context
 val unpackage : 'a sigma -> evar_map ref * 'a
 val repackage : evar_map ref -> 'a -> 'a sigma
 val apply_sig_tac :
-  evar_map ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c
+  evar_map ref -> (goal sigma -> (goal list) sigma * validation) -> goal -> (goal list) * validation
 
 type transformation_tactic = proof_tree -> (goal list * validation)
 
@@ -40,15 +40,16 @@ val abstract_operation : compound_rule -> tactic -> tactic
 val abstract_tactic : ?dflt:bool -> atomic_tactic_expr -> tactic -> tactic
 val abstract_tactic_expr : ?dflt:bool -> tactic_expr -> tactic -> tactic
 val abstract_extended_tactic :
-  ?dflt:bool -> string -> closed_generic_argument list -> tactic -> tactic
+  ?dflt:bool -> string -> typed_generic_argument list -> tactic -> tactic
 
 val refiner : rule -> tactic
 val frontier : transformation_tactic
 val list_pf : proof_tree -> goal list
 val unTAC : tactic -> goal sigma -> proof_tree sigma
 
-val local_Constraints : tactic
 
+(* Install a hook frontier_map and frontier_mapi call on the new node they create *)
+val set_solve_hook : (Proof_type.proof_tree -> unit) -> unit
 (* [frontier_map f n p] applies f on the n-th open subgoal of p and
    rebuilds proof-tree.
    n=1 for first goal, n negative counts from the right *)
@@ -61,6 +62,9 @@ val frontier_mapi :
 
 (*s Tacticals. *)
 
+(* [tclNORMEVAR] forces propagation of evar constraints *)
+val tclNORMEVAR       : tactic
+
 (* [tclIDTAC] is the identity tactic without message printing*)
 val tclIDTAC          : tactic
 val tclIDTAC_MESSAGE  : Pp.std_ppcmds -> tactic
@@ -100,6 +104,13 @@ val tclTHENS         : tactic -> tactic list -> tactic
 val tclTHENST        : tactic -> tactic array -> tactic -> tactic
 *)
 
+(* [tclTHENS3PARTS tac1 [|t1 ; ... ; tn|] tac2 [|t'1 ; ... ; t'm|] gls]
+   applies the tactic [tac1] to [gls] then, applies [t1], ..., [tn] to
+   the first [n] resulting subgoals, [t'1], ..., [t'm] to the last [m]
+   subgoals and [tac2] to the rest of the subgoals in the middle. Raises an
+   error if the number of resulting subgoals is strictly less than [n+m] *)
+val tclTHENS3PARTS     : tactic -> tactic array -> tactic -> tactic array -> tactic
+
 (* [tclTHENSLASTn tac1 [t1 ; ... ; tn] tac2 gls] applies [t1],...,[tn] on the
    last [n] resulting subgoals and [tac2] on the remaining first subgoals *)
 val tclTHENSLASTn     : tactic -> tactic -> tactic array -> tactic
@@ -122,6 +133,10 @@ val tclTHENFIRSTn   : tactic -> tactic array -> tactic
 (* A special exception for levels for the Fail tactic *)
 exception FailError of int * Pp.std_ppcmds
 
+(* Takes an exception and either raise it at the next
+   level or do nothing. *)
+val catch_failerror  : exn -> unit
+
 val tclORELSE        : tactic -> tactic -> tactic
 val tclREPEAT        : tactic -> tactic
 val tclREPEAT_MAIN   : tactic -> tactic
@@ -189,6 +204,7 @@ val solve_pftreestate : tactic -> pftreestate -> pftreestate
 val weak_undo_pftreestate : pftreestate -> pftreestate
 
 val mk_pftreestate : goal -> pftreestate
+val extract_open_proof : evar_map -> proof_tree -> constr * (int * types) list
 val extract_open_pftreestate : pftreestate -> constr * Termops.metamap
 val extract_pftreestate : pftreestate -> constr
 val first_unproven : pftreestate -> pftreestate
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 0bcc7d16..d0789980 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 9551 2007-01-29 15:13:35Z bgregoir $ i*)
+(*i $Id: tacexpr.ml 11100 2008-06-11 11:10:31Z herbelin $ i*)
 
 open Names
 open Topconstr
@@ -16,18 +16,25 @@ open Rawterm
 open Util
 open Genarg
 open Pattern
+open Decl_kinds
 
 type 'a or_metaid = AI of 'a | MetaId of loc * string
 
 type direction_flag = bool (* true = Left-to-right    false = right-to-right *)
 type lazy_flag = bool      (* true = lazy             false = eager *)
+type evars_flag = bool     (* true = pose evars       false = fail on evars *)
+type rec_flag = bool       (* true = recursive        false = not recursive *)
+type advanced_flag = bool  (* true = advanced         false = basic *)
+type split_flag = bool     (* true = exists           false = split *)
+type hidden_flag = bool    (* true = internal use     false = user-level *)
+type letin_flag = bool     (* true = use local def    false = use Leibniz *)
 
 type raw_red_flag =
   | FBeta
   | FIota
   | FZeta
-  | FConst of reference list
-  | FDeltaBut of reference list
+  | FConst of reference or_by_notation list
+  | FDeltaBut of reference or_by_notation list
 
 let make_red_flag =
   let rec add_flag red = function
@@ -87,15 +94,23 @@ type 'id gsimple_clause = ('id raw_hyp_location) option
      [Some l] means on hypothesis belonging to l *)
 type 'id gclause =
   { onhyps : 'id raw_hyp_location list option;
-    onconcl : bool;
-    concl_occs : int or_var list }
+    concl_occs : bool * int or_var list }
 
-let nowhere = {onhyps=Some[]; onconcl=false; concl_occs=[]}
+let nowhere = {onhyps=Some[]; concl_occs=no_occurrences_expr}
 
 let simple_clause_of = function
-    { onhyps = Some[scl]; onconcl = false } -> Some scl
-  | { onhyps = Some []; onconcl = true; concl_occs=[] } -> None
-  | _ -> error "not a simple clause (one hypothesis or conclusion)"
+| { onhyps = Some [scl]; concl_occs = occs } when occs = no_occurrences_expr ->
+      Some scl
+| { onhyps = Some []; concl_occs = occs } when occs = all_occurrences_expr ->
+    None
+| _ ->
+    error "not a simple clause (one hypothesis or conclusion)"
+
+type multi = 
+  | Precisely of int
+  | UpTo of int
+  | RepeatStar
+  | RepeatPlus
 
 type pattern_expr = constr_expr
 
@@ -122,29 +137,30 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacExact of 'constr
   | TacExactNoCheck of 'constr
   | TacVmCastNoCheck of 'constr
-  | TacApply of 'constr with_bindings
-  | TacElim of 'constr with_bindings * 'constr with_bindings option
+  | TacApply of advanced_flag * evars_flag * 'constr with_bindings
+  | TacElim of evars_flag * 'constr with_bindings * 
+      'constr with_bindings option
   | TacElimType of 'constr
-  | TacCase of 'constr with_bindings
+  | TacCase of evars_flag * 'constr with_bindings
   | TacCaseType of 'constr
   | TacFix of identifier option * int
-  | TacMutualFix of identifier * int * (identifier * int * 'constr) list
+  | TacMutualFix of hidden_flag * identifier * int * (identifier * int * 
+      'constr) list
   | TacCofix of identifier option
-  | TacMutualCofix of identifier * (identifier * 'constr) list
+  | TacMutualCofix of hidden_flag * identifier * (identifier * 'constr) list
   | TacCut of 'constr
   | TacAssert of 'tac option * intro_pattern_expr * 'constr
-  | TacGeneralize of 'constr list
+  | TacGeneralize of ('constr with_occurrences * name) list
   | TacGeneralizeDep of 'constr
-  | TacLetTac of name * 'constr * 'id gclause
-(*  | TacInstantiate of int * 'constr * (('id * hyp_location_flag,unit) location) *)
+  | TacLetTac of name * 'constr * 'id gclause * letin_flag
 
   (* Derived basic tactics *)
   | TacSimpleInduction of quantified_hypothesis
-  | TacNewInduction of 'constr induction_arg list * 'constr with_bindings option
-      * intro_pattern_expr
+  | 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 'constr induction_arg list * 'constr with_bindings option
-      * intro_pattern_expr
+  | TacNewDestruct of evars_flag * 'constr with_bindings induction_arg list *
+      'constr with_bindings option * intro_pattern_expr * 'id gclause option
 
   | TacDoubleInduction of quantified_hypothesis * quantified_hypothesis
   | TacDecomposeAnd of 'constr
@@ -160,20 +176,21 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacDestructHyp of (bool * identifier located)
   | TacDestructConcl
   | TacSuperAuto of (int option * reference list * bool * bool)
-  | TacDAuto of int or_var option * int option
+  | TacDAuto of int or_var option * int option * 'constr list
 
   (* Context management *)
   | TacClear of bool * 'id list
   | TacClearBody of 'id list
   | TacMove of bool * 'id * 'id
-  | TacRename of 'id * 'id
+  | TacRename of ('id *'id) list
+  | TacRevert of 'id list
 
   (* Constructors *)
-  | TacLeft of 'constr bindings
-  | TacRight of 'constr bindings
-  | TacSplit of bool * 'constr bindings
-  | TacAnyConstructor of 'tac option
-  | TacConstructor of int or_metaid * 'constr bindings
+  | TacLeft of evars_flag * 'constr bindings
+  | TacRight of evars_flag * 'constr bindings
+  | TacSplit of evars_flag * split_flag * 'constr bindings
+  | TacAnyConstructor of evars_flag * 'tac option
+  | TacConstructor of evars_flag * int or_metaid * 'constr bindings
 
   (* Conversion *)
   | TacReduce of ('constr,'cst) red_expr_gen * 'id gclause
@@ -185,21 +202,26 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacTransitivity of 'constr 
 
   (* Equality and inversion *)
-  | TacRewrite of bool * 'constr with_bindings * 'id gclause
+  | TacRewrite of 
+      evars_flag * (bool * multi * 'constr with_bindings) list * 'id gclause * 'tac option
   | TacInversion of ('constr,'id) inversion_strength * quantified_hypothesis
       
   (* For ML extensions *)
-  | TacExtend of loc * string * ('constr,'tac) generic_argument list
+  | TacExtend of loc * string * 'constr generic_argument list
 
   (* For syntax extensions *)
   | TacAlias of loc * string *
-      (identifier * ('constr,'tac) generic_argument) list
+      (identifier * 'constr generic_argument) list
       * (dir_path * glob_tactic_expr)
 
 and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
   | TacAtom of loc * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr
-  | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
-  | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
+  | TacThen of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * 
+	('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr array *
+	('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr *
+	('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr array
+  | TacThens of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr * 
+	('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
   | TacFirst of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
   | TacComplete of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
   | TacSolve of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr list
@@ -212,8 +234,7 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
   | TacId of 'id message_token list
   | TacFail of int or_var * 'id message_token list
   | TacInfo of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
-  | TacLetRecIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast) list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
-  | TacLetIn of (identifier located * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr option * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg) list * ('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
   | TacFun of ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast
@@ -222,11 +243,11 @@ and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr =
 and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_fun_ast =
   identifier option list * ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_expr
 
-  (* These are possible arguments of a tactic definition *)
+  (* These are the possible arguments of a tactic definition *)
 and ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_tactic_arg =
   | TacDynamic     of loc * Dyn.t
   | TacVoid
-  | MetaIdArg      of loc * string
+  | MetaIdArg      of loc * bool * string
   | ConstrMayEval  of ('constr,'cst) may_eval
   | IntroPattern   of intro_pattern_expr
   | Reference      of 'ref
@@ -251,8 +272,8 @@ and glob_tactic_expr =
 type raw_tactic_expr =
     (constr_expr,
      pattern_expr,
-     reference,
-     reference,
+     reference or_by_notation,
+     reference or_by_notation,
      reference,
      identifier located or_metaid,
      raw_tactic_expr) gen_tactic_expr
@@ -260,8 +281,8 @@ type raw_tactic_expr =
 type raw_atomic_tactic_expr =
     (constr_expr,                  (* constr *)
      pattern_expr,                 (* pattern *)
-     reference,                    (* evaluable reference *)
-     reference,                    (* inductive *)
+     reference or_by_notation,     (* evaluable reference *)
+     reference or_by_notation,     (* inductive *)
      reference,                    (* ltac reference *)
      identifier located or_metaid, (* identifier *)
      raw_tactic_expr) gen_atomic_tactic_expr
@@ -269,16 +290,15 @@ type raw_atomic_tactic_expr =
 type raw_tactic_arg =
     (constr_expr,
      pattern_expr,
-     reference,
-     reference,
+     reference or_by_notation,
+     reference or_by_notation,
      reference,
      identifier located or_metaid,
      raw_tactic_expr) gen_tactic_arg
 
-type raw_generic_argument =
-    (constr_expr,raw_tactic_expr) generic_argument
+type raw_generic_argument = constr_expr generic_argument
 
-type raw_red_expr = (constr_expr, reference) red_expr_gen
+type raw_red_expr = (constr_expr, reference or_by_notation) red_expr_gen
 
 type glob_atomic_tactic_expr =
     (rawconstr_and_expr,
@@ -298,28 +318,17 @@ type glob_tactic_arg =
      identifier located,
      glob_tactic_expr) gen_tactic_arg
 
-type glob_generic_argument =
-    (rawconstr_and_expr,glob_tactic_expr) generic_argument
+type glob_generic_argument = rawconstr_and_expr generic_argument
 
 type glob_red_expr =
     (rawconstr_and_expr, evaluable_global_reference or_var) red_expr_gen
 
-type closed_raw_generic_argument =
-    (constr_expr,raw_tactic_expr) generic_argument
-
-type 'a raw_abstract_argument_type =
-    ('a,rlevel,raw_tactic_expr) abstract_argument_type
-
-type 'a glob_abstract_argument_type =
-    ('a,glevel,glob_tactic_expr) abstract_argument_type
+type typed_generic_argument = Evd.open_constr generic_argument
 
-type open_generic_argument =
-    (Term.constr,glob_tactic_expr) generic_argument
+type 'a raw_abstract_argument_type = ('a,rlevel) abstract_argument_type
 
-type closed_generic_argument =
-    (Term.constr,glob_tactic_expr) generic_argument
+type 'a glob_abstract_argument_type = ('a,glevel) abstract_argument_type
 
-type 'a closed_abstract_argument_type =
-    ('a,Term.constr,glob_tactic_expr) abstract_argument_type
+type 'a typed_abstract_argument_type = ('a,tlevel) abstract_argument_type
 
-type declaration_hook = Decl_kinds.strength -> global_reference -> unit
+type declaration_hook = locality -> global_reference -> unit
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index baf8c859..213cc13f 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacmach.ml 9511 2007-01-22 08:27:31Z herbelin $ *)
+(* $Id: tacmach.ml 10544 2008-02-09 11:31:35Z herbelin $ *)
 
 open Util
 open Names
@@ -205,8 +205,11 @@ let thin_body_no_check ids gl =
 let move_hyp_no_check with_dep id1 id2 gl = 
   refiner (Prim (Move (with_dep,id1,id2))) gl
 
-let rename_hyp_no_check id1 id2 gl = 
-  refiner (Prim (Rename (id1,id2))) gl
+let rec rename_hyp_no_check l gl = match l with 
+  | [] -> tclIDTAC gl 
+  | (id1,id2)::l -> 
+      tclTHEN (refiner (Prim (Rename (id1,id2)))) 
+	(rename_hyp_no_check l) gl
 
 let mutual_fix f n others gl = 
   with_check (refiner (Prim (FixRule (f,n,others)))) gl
@@ -214,14 +217,6 @@ let mutual_fix f n others gl =
 let mutual_cofix f others gl = 
   with_check (refiner (Prim (Cofix (f,others)))) gl
     
-let rename_bound_var_goal gls =
-  let { evar_hyps = sign; evar_concl = cl } = sig_it gls in 
-  let ids = ids_of_named_context (named_context_of_val sign) in
-  convert_concl_no_check 
-    (rename_bound_var (Global.env()) ids cl) DEFAULTcast gls 
-
-
-
 (* Versions with consistency checks *)
 
 let introduction id    = with_check (introduction_no_check id) 
@@ -234,8 +229,8 @@ let convert_hyp d      = with_check (convert_hyp_no_check d)
 let thin l             = with_check (thin_no_check l)
 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 id id'  = with_check (rename_hyp_no_check id id')
-    
+let rename_hyp l       = with_check (rename_hyp_no_check l)
+
 (* Pretty-printers *)
 
 open Pp
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 9352cb5d..8b0053a4 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 7639 2005-12-02 10:01:15Z gregoire $ i*)
+(*i $Id: tacmach.mli 11094 2008-06-10 19:35:23Z herbelin $ i*)
 
 (*i*)
 open Names
@@ -37,7 +37,7 @@ val re_sig : 'a -> evar_map -> 'a sigma
 val unpackage : 'a sigma -> evar_map ref * 'a
 val repackage : evar_map ref -> 'a -> 'a sigma
 val apply_sig_tac :
-  evar_map ref -> ('a sigma -> 'b sigma * 'c) -> 'a -> 'b * 'c
+  evar_map ref -> (goal sigma -> (goal list) sigma * validation) -> goal -> (goal list) * validation
 
 val pf_concl              : goal sigma -> types
 val pf_env                : goal sigma -> env
@@ -79,7 +79,7 @@ val pf_nf_betaiota             : goal sigma -> constr -> constr
 val pf_reduce_to_quantified_ind : goal sigma -> types -> inductive * types
 val pf_reduce_to_atomic_ind     : goal sigma -> types -> inductive * types
 val pf_compute                 : goal sigma -> constr -> constr
-val pf_unfoldn    : (int list * evaluable_global_reference) list
+val pf_unfoldn    : (Termops.occurrences * evaluable_global_reference) list
         -> goal sigma -> constr -> constr
 
 val pf_const_value : goal sigma -> constant -> constr
@@ -132,11 +132,10 @@ 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 rename_hyp_no_check       : identifier -> identifier -> tactic
+val rename_hyp_no_check       : (identifier*identifier) list -> tactic
 val mutual_fix      :
   identifier -> int -> (identifier * int * constr) list -> tactic
 val mutual_cofix    : identifier -> (identifier * constr) list -> tactic
-val rename_bound_var_goal : tactic
 
 (*s The most primitive tactics with consistency and type checking *)
 
@@ -150,7 +149,7 @@ 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 rename_hyp       : identifier -> identifier -> tactic
+val rename_hyp       : (identifier*identifier) list -> tactic
 
 (*s Tactics handling a list of goals. *)
 
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 96df8f64..2e19011f 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -6,6 +6,8 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
+(*i $Id: tactic_debug.ml 10739 2008-04-01 14:45:20Z herbelin $ i*)
+
 open Names
 open Constrextern
 open Pp