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

16 files changed, 223 insertions, 111 deletions

diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index 92794ac3..f5204be5 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: clenvtac.ml 11166 2008-06-22 13:23:35Z herbelin $ *)
+(* $Id: clenvtac.ml 11709 2008-12-20 11:42:15Z msozeau $ *)
 
 open Pp
 open Util
@@ -47,16 +47,17 @@ let clenv_cast_meta clenv =
 	    
   and crec_hd u =
     match kind_of_term (strip_outer_cast u) with
-      | Meta mv ->
-	  (try 
+    | Meta mv ->
+	(try 
             let b = Typing.meta_type clenv.evd mv in
-	    if occur_meta b then u
-            else mkCast (mkMeta mv, DEFAULTcast, b)
+	      if occur_meta b then
+		raise (RefinerError (MetaInType b));
+	      mkCast (mkMeta mv, DEFAULTcast, b)
 	  with Not_found -> u)
-      | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
-      | Case(ci,p,c,br) ->
-	  mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
-      | _ -> u
+    | App(f,args) -> mkApp (crec_hd f, Array.map crec args)
+    | Case(ci,p,c,br) ->
+	mkCase (ci, crec_hd p, crec_hd c, Array.map crec br)
+    | _ -> u
   in 
   crec
 
@@ -71,10 +72,15 @@ let clenv_pose_dependent_evars with_evars clenv =
   clenv_pose_metas_as_evars clenv dep_mvs
 
 
-let clenv_refine with_evars clenv gls =
+let clenv_refine with_evars ?(with_classes=true) clenv gls =
   let clenv = clenv_pose_dependent_evars with_evars clenv in
+  let evd' = 
+    if with_classes then 
+      Typeclasses.resolve_typeclasses ~fail:(not with_evars) clenv.env clenv.evd 
+    else clenv.evd
+  in
   tclTHEN
-    (tclEVARS (evars_of clenv.evd)) 
+    (tclEVARS (evars_of evd')) 
     (refine (clenv_cast_meta clenv (clenv_value clenv)))
     gls
 
@@ -105,11 +111,11 @@ let fail_quick_unif_flags = {
 }
 
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
-let unifyTerms m n gls = 
+let unifyTerms ?(flags=fail_quick_unif_flags) m n gls = 
   let env = pf_env gls 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
+  let evd' = w_unify false env CONV ~flags m n evd in
   tclIDTAC {it = gls.it; sigma = evars_of evd'}
 
-let unify m gls =
-  let n = pf_concl gls in unifyTerms m n gls
+let unify ?(flags=fail_quick_unif_flags) m gls =
+  let n = pf_concl gls in unifyTerms ~flags m n gls
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index 29442ded..04a5eb57 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 11166 2008-06-22 13:23:35Z herbelin $ i*)
+(*i $Id: clenvtac.mli 11709 2008-12-20 11:42:15Z msozeau $ i*)
 
 (*i*)
 open Util
@@ -21,8 +21,8 @@ open Unification
 (*i*)
 
 (* Tactics *)
-val unify : constr -> tactic
-val clenv_refine : evars_flag -> clausenv -> tactic
+val unify : ?flags:unify_flags -> constr -> tactic
+val clenv_refine : evars_flag -> ?with_classes:bool -> 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
 
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 21ee9a9f..a04216cb 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: logic.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: logic.ml 11796 2009-01-18 13:41:39Z herbelin $ *)
 
 open Pp
 open Util
@@ -37,6 +37,7 @@ type refiner_error =
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
+  | MetaInType of constr
 
   (* Errors raised by the tactics *)
   | IntroNeedsProduct
@@ -57,29 +58,18 @@ let rec catchable_exception = function
 		   |NoOccurrenceFound _|CannotUnifyBindingType _|NotClean _
 		   |CannotFindWellTypedAbstraction _
 		   |UnsolvableImplicit _)) -> true
+  | Typeclasses_errors.TypeClassError 
+      (_, Typeclasses_errors.UnsatisfiableConstraints _) -> true
   | _ -> false
 
+let error_no_such_hypothesis id =
+  error ("No such hypothesis: " ^ string_of_id id ^ ".")
+
 (* Tells if the refiner should check that the submitted rules do not
    produce invalid subgoals *)
 let check = ref false
 let with_check = Flags.with_option check
 
-(************************************************************************)
-(************************************************************************)
-(* Implementation of the structural rules (moving and deleting
-   hypotheses around) *)
-
-(* 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 sign cl =
-  let evdref = ref (Evd.create_goal_evar_defs sigma) in
-  let (hyps,concl) = Evarutil.clear_hyps_in_evi evdref sign cl ids in
-  (hyps,concl,evars_of !evdref)
-
-(* The ClearBody tactic *)
-
 (* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and
    returns [tail::(f head (id,_,_) (rev tail))] *)
 let apply_to_hyp sign id f =
@@ -97,6 +87,22 @@ let apply_to_hyp_and_dependent_on sign id f g =
 let check_typability env sigma c =
   if !check then let _ = type_of env sigma c in () 
 
+(************************************************************************)
+(************************************************************************)
+(* Implementation of the structural rules (moving and deleting
+   hypotheses around) *)
+
+(* 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 sign cl =
+  let evdref = ref (Evd.create_goal_evar_defs sigma) in
+  let (hyps,concl) = Evarutil.clear_hyps_in_evi evdref sign cl ids in
+  (hyps,concl,evars_of !evdref)
+
+(* The ClearBody tactic *)
+
 let recheck_typability (what,id) env sigma t =
   try check_typability env sigma t
   with _ ->
@@ -126,6 +132,82 @@ let remove_hyp_body env sigma id =
   in
   reset_with_named_context sign env 
 
+(* Reordering of the context *)
+
+(* faire le minimum d'echanges pour que l'ordre donne soit un *)
+(* sous-ordre du resultat. Par exemple, 2 hyps non mentionnee ne sont *)
+(* pas echangees. Choix: les hyps mentionnees ne peuvent qu'etre *)
+(* reculees par rapport aux autres (faire le contraire!) *)
+ 
+let mt_q = (Idmap.empty,[])
+let push_val y = function
+    (_,[] as q) -> q
+  | (m, (x,l)::q) -> (m, (x,Idset.add y l)::q)
+let push_item x v (m,l) =
+  (Idmap.add x v m, (x,Idset.empty)::l)
+let mem_q x (m,_) = Idmap.mem x m
+let rec find_q x (m,q) =
+  let v = Idmap.find x m in
+  let m' = Idmap.remove x m in
+  let rec find accs acc = function
+      [] -> raise Not_found
+    | [(x',l)] ->
+        if x=x' then ((v,Idset.union accs l),(m',List.rev acc))
+        else raise Not_found
+    | (x',l as i)::((x'',l'')::q as itl) ->
+        if x=x' then
+          ((v,Idset.union accs l),
+           (m',List.rev acc@(x'',Idset.add x (Idset.union l l''))::q))
+        else find (Idset.union l accs) (i::acc) itl in
+  find Idset.empty [] q
+
+let occur_vars_in_decl env hyps d =
+  if Idset.is_empty hyps then false else
+    let ohyps = global_vars_set_of_decl env d in
+    Idset.exists (fun h -> Idset.mem h ohyps) hyps
+
+let reorder_context env sign ord =
+  let ords = List.fold_right Idset.add ord Idset.empty in
+  if List.length ord <> Idset.cardinal ords then
+    error "Order list has duplicates";
+  let rec step ord expected ctxt_head moved_hyps ctxt_tail =
+    match ord with
+      | [] -> List.rev ctxt_tail @ ctxt_head
+      | top::ord' when mem_q top moved_hyps ->
+          let ((d,h),mh) = find_q top moved_hyps in
+          if occur_vars_in_decl env h d then
+            errorlabstrm "reorder_context"
+              (str "Cannot move declaration " ++ pr_id top ++ spc() ++
+              str "before " ++
+              prlist_with_sep pr_spc pr_id
+                (Idset.elements (Idset.inter h
+                  (global_vars_set_of_decl env d))));
+          step ord' expected ctxt_head mh (d::ctxt_tail)
+      | _ ->
+          (match ctxt_head with
+            | [] -> error_no_such_hypothesis (List.hd ord)
+            | (x,_,_ as d) :: ctxt ->
+                if Idset.mem x expected then
+                  step ord (Idset.remove x expected)
+                    ctxt (push_item x d moved_hyps) ctxt_tail
+                else
+                  step ord expected
+                    ctxt (push_val x moved_hyps) (d::ctxt_tail)) in
+  step ord ords sign mt_q []
+
+let reorder_val_context env sign ord =
+  val_of_named_context (reorder_context env (named_context_of_val sign) ord)
+
+
+
+
+let check_decl_position env sign (x,_,_ as d) =
+  let needed = global_vars_set_of_decl env d in
+  let deps = dependency_closure env (named_context_of_val sign) needed in
+  if List.mem x deps then
+    error ("Cannot create self-referring hypothesis "^string_of_id x);
+  x::deps
+
 (* Auxiliary functions for primitive MOVE tactic
  *
  * [move_hyp with_dep toleft (left,(hfrom,typfrom),right) hto] moves
@@ -134,9 +216,6 @@ let remove_hyp_body env sigma id =
  * 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 ->
@@ -219,14 +298,23 @@ let rename_hyp id1 id2 sign =
 (* Will only be used on terms given to the Refine rule which have meta 
 variables only in Application and Case *)
 
+let error_unsupported_deep_meta c =
+  errorlabstrm "" (strbrk "Application of lemmas whose beta-iota normal " ++
+    strbrk "form contains metavariables deep inside the term is not " ++
+    strbrk "supported; try \"refine\" instead.")
+
 let collect_meta_variables c = 
-  let rec collrec acc c = match kind_of_term c with
-    | Meta mv -> mv::acc
-    | Cast(c,_,_) -> collrec acc c
-    | (App _| Case _) -> fold_constr collrec acc c
-    | _ -> acc
-  in 
-  List.rev(collrec [] c)
+  let rec collrec deep acc c = match kind_of_term c with
+    | Meta mv -> if deep then error_unsupported_deep_meta () else mv::acc
+    | Cast(c,_,_) -> collrec deep acc c
+    | (App _| Case _) -> fold_constr (collrec deep) acc c
+    | _ -> fold_constr (collrec true) acc c
+  in
+  List.rev (collrec false [] c)
+
+let check_meta_variables c = 
+  if not (list_distinct (collect_meta_variables c)) then
+    raise (RefinerError (NonLinearProof c))
 
 let check_conv_leq_goal env sigma arg ty conclty =
   if !check & not (is_conv_leq env sigma ty conclty) then 
@@ -248,9 +336,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 *)
   match kind_of_term trm with
     | Meta _ ->
-	if !check && occur_meta conclty then
-	  anomaly "refined called with a dependent meta";
-	(mk_goal hyps (nf_betaiota conclty))::goalacc, conclty
+	let conclty = nf_betaiota conclty in
+	  if !check && occur_meta conclty then
+	    raise (RefinerError (MetaInType conclty));
+	  (mk_goal hyps conclty)::goalacc, conclty
 
     | Cast (t,_, ty) ->
 	check_typability env sigma ty;
@@ -261,12 +350,10 @@ let rec mk_refgoals sigma goal goalacc conclty trm =
 	let (acc',hdty) =
 	  match kind_of_term f with
 	    | Ind _ | Const _
-		when not (array_exists occur_meta l) (* we could be finer *)
-		  & (isInd f or has_polymorphic_type (destConst f))
-		  ->
+		when (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
+                type_of_global_reference_knowing_conclusion env sigma f conclty
 	    | _ -> 
 		mk_hdgoals sigma goal goalacc f
 	in
@@ -288,6 +375,7 @@ let rec mk_refgoals sigma goal goalacc conclty 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)
@@ -358,14 +446,19 @@ and mk_casegoals sigma goal goalacc p c =
 
 
 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)^".");
-       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)
+  let env = Global.env() in
+  let reorder = ref [] in
+  let sign' =
+    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)^".");
+        if !check && not (Option.Misc.compare (is_conv env sigma) b c) then
+	  error ("Incorrect change of the body of "^(string_of_id id)^".");
+       if !check then reorder := check_decl_position env sign d;
+       d) in
+  reorder_val_context env sign' !reorder
 
 (* Normalizing evars in a goal. Called by tactic Local_constraints
    (i.e. when the sigma of the proof tree changes). Detect if the
@@ -418,7 +511,9 @@ let prim_refiner r sigma goal =
 	      nexthyp,
 	      cl,sigma
 	  else
-	    (push_named_context_val (id,None,t) sign),cl,sigma in
+            (if !check && mem_named_context id (named_context_of_val sign) then
+                error "New variable is already declared";
+	     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)
 
@@ -478,8 +573,7 @@ let prim_refiner r sigma goal =
 	  (mk_sign sign all, sigma)
 
     | Refine c ->
-        if not (list_distinct (collect_meta_variables c)) then
-          raise (RefinerError (NonLinearProof c));
+	check_meta_variables c;
 	let (sgl,cl') = mk_refgoals sigma goal [] cl c in
 	let sgl = List.rev sgl in
 	  (sgl, sigma)
@@ -518,6 +612,10 @@ let prim_refiner r sigma goal =
 	  move_hyp withdep toleft (left,declfrom,right) hto in
   	  ([mk_goal hyps' cl], sigma)
 
+    | Order ord ->
+        let hyps' = reorder_val_context env sign ord 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
@@ -628,7 +726,7 @@ let prim_extractor subfun vl pft =
       | Some (Prim (ThinBody _),[pf]) ->
 	  subfun vl pf
 	    
-      | Some (Prim (Move _),[pf]) ->
+      | Some (Prim (Move _|Order _),[pf]) ->
 	  subfun vl pf
 
       | Some (Prim (Rename (id1,id2)),[pf]) ->
diff --git a/proofs/logic.mli b/proofs/logic.mli
index def02c8c..2f3a0d89 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 10785 2008-04-13 21:41:54Z herbelin $ i*)
+(*i $Id: logic.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
 
 (*i*)
 open Names
@@ -54,6 +54,7 @@ type refiner_error =
   | CannotApply of constr * constr
   | NotWellTyped of constr
   | NonLinearProof of constr
+  | MetaInType of constr
 
   (*i Errors raised by the tactics i*)
   | IntroNeedsProduct
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 6d8f09ea..0aba9f5f 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: pfedit.ml 10850 2008-04-25 18:07:44Z herbelin $ *)
+(* $Id: pfedit.ml 11745 2009-01-04 18:43:08Z herbelin $ *)
 
 open Pp
 open Util
@@ -34,6 +34,7 @@ open Safe_typing
 type proof_topstate = {
   mutable top_end_tac : tactic option;
   top_init_tac : tactic option;
+  top_compute_guard : bool;
   top_goal : goal;
   top_strength : Decl_kinds.goal_kind;
   top_hook : declaration_hook }
@@ -207,7 +208,7 @@ let set_xml_cook_proof f = xml_cook_proof := f
 let cook_proof k =
   let (pfs,ts) = get_state() 
   and ident = get_current_proof_name () in
-  let {evar_concl=concl} = ts.top_goal 
+  let {evar_concl=concl} = ts.top_goal
   and strength = ts.top_strength in
   let pfterm = extract_pftreestate pfs in
   !xml_cook_proof (strength,pfs);
@@ -217,7 +218,7 @@ let cook_proof k =
       const_entry_type = Some concl;
       const_entry_opaque = true;
       const_entry_boxed = false},
-    strength, ts.top_hook))
+    ts.top_compute_guard, strength, ts.top_hook))
 
 let current_proof_statement () = 
   let ts = get_topstate() in
@@ -251,11 +252,12 @@ let set_end_tac tac =
 (*              Modifying the current prooftree                      *)
 (*********************************************************************)
 
-let start_proof na str sign concl ?init_tac hook =
+let start_proof na str sign concl ?init_tac ?(compute_guard=false) hook =
   let top_goal = mk_goal sign concl None in
   let ts = { 
     top_end_tac = None;
     top_init_tac = init_tac;
+    top_compute_guard = compute_guard;
     top_goal = top_goal;
     top_strength = str;
     top_hook = hook}
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index 42c24081..464f6286 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 10850 2008-04-25 18:07:44Z herbelin $ i*)
+(*i $Id: pfedit.mli 11745 2009-01-04 18:43:08Z herbelin $ i*)
 
 (*i*)
 open Util
@@ -80,7 +80,7 @@ val get_undo : unit -> int option
 
 val start_proof : 
   identifier -> goal_kind -> named_context_val -> constr ->
-    ?init_tac:tactic -> declaration_hook -> unit
+    ?init_tac:tactic -> ?compute_guard:bool -> declaration_hook -> unit
 
 (* [restart_proof ()] restarts the current focused proof from the beginning
    or fails if no proof is focused *)
@@ -104,10 +104,11 @@ val suspend_proof : unit -> unit
 
 (*s [cook_proof opacity] turns the current proof (assumed completed) into
     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 *)
+    it fails if there is no current proof of if it is not completed;
+    it also tells if the guardness condition has to be inferred. *)
 
 val cook_proof : (Refiner.pftreestate -> unit) -> 
-  identifier * (Entries.definition_entry * goal_kind * declaration_hook)
+  identifier * (Entries.definition_entry * bool * goal_kind * declaration_hook)
 
 (* To export completed proofs to xml *)
 val set_xml_cook_proof : (goal_kind * pftreestate -> unit) -> unit
diff --git a/proofs/proof_type.ml b/proofs/proof_type.ml
index 41935c9c..1e673853 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 11309 2008-08-06 10:30:35Z herbelin $ *)
+(*i $Id: proof_type.ml 11639 2008-11-27 17:48:32Z barras $ *)
 
 (*i*)
 open Environ
@@ -37,6 +37,7 @@ type prim_rule =
   | Thin of identifier list
   | ThinBody of identifier list
   | Move of bool * identifier * identifier move_location
+  | Order of identifier list
   | Rename of identifier * identifier
   | Change_evars
 
diff --git a/proofs/proof_type.mli b/proofs/proof_type.mli
index a7057a7d..21cd8b28 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 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: proof_type.mli 11639 2008-11-27 17:48:32Z barras $ i*)
 
 (*i*)
 open Environ
@@ -37,6 +37,7 @@ type prim_rule =
   | Thin of identifier list
   | ThinBody of identifier list
   | Move of bool * identifier * identifier move_location
+  | Order of identifier list
   | Rename of identifier * identifier
   | Change_evars
 
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 072a38b6..ad8ee3a2 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: redexpr.ml 11094 2008-06-10 19:35:23Z herbelin $ *)
+(* $Id: redexpr.ml 11481 2008-10-20 19:23:51Z herbelin $ *)
 
 open Pp
 open Util
@@ -46,12 +46,13 @@ let set_strategy_one ref l  =
         Csymtable.set_transparent_const sp
     | _ -> ()
 
-let cache_strategy str =
+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) =
+let subst_strategy (_,subs,(local,obj)) =
+  local,
   list_smartmap
     (fun (k,ql as entry) ->
       let ql' = list_smartmap (Mod_subst.subst_evaluable_reference subs) ql in
@@ -68,14 +69,16 @@ let map_strategy f l =
               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'
+  if l'=[] then None else Some (false,l')
 
-let export_strategy obj =
+let export_strategy (local,obj) =
+  if local then None else
   map_strategy (function
       EvalVarRef _ -> None
     | EvalConstRef _ as q -> Some q) obj
 
-let classify_strategy (_,obj) = Substitute obj
+let classify_strategy (_,(local,_ as obj)) = 
+  if local then Dispose else Substitute obj
 
 let disch_ref ref =
   match ref with
@@ -84,7 +87,8 @@ let disch_ref ref =
         if c==c' then Some ref else Some (EvalConstRef c')
     | _ -> Some ref
 
-let discharge_strategy (_,obj) =
+let discharge_strategy (_,(local,obj)) =
+  if local then None else
   map_strategy disch_ref obj
 
 let (inStrategy,outStrategy) =
@@ -98,8 +102,7 @@ let (inStrategy,outStrategy) =
 
 
 let set_strategy local str =
-  if local then cache_strategy str
-  else Lib.add_anonymous_leaf (inStrategy str)
+  Lib.add_anonymous_leaf (inStrategy (local,str))
 
 let _ = 
   Summary.declare_summary "Transparent constants and variables"
diff --git a/proofs/refiner.ml b/proofs/refiner.ml
index 6e08e741..a9a1f51d 100644
--- a/proofs/refiner.ml
+++ b/proofs/refiner.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: refiner.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: refiner.ml 11865 2009-01-28 17:34:30Z herbelin $ *)
 
 open Pp
 open Util
@@ -462,7 +462,7 @@ let weak_progress gls ptree =
   (not (same_goal (List.hd gls.it) ptree.it))
 
 let progress gls ptree =
-  (not (ptree.sigma == gls.sigma)) ||
+  (not (eq_evar_map ptree.sigma gls.sigma)) ||
   (weak_progress gls ptree)
 
 
diff --git a/proofs/refiner.mli b/proofs/refiner.mli
index 95130ac5..a6ba3af5 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 10879 2008-05-01 22:14:20Z msozeau $ i*)
+(*i $Id: refiner.mli 11735 2009-01-02 17:22:31Z herbelin $ i*)
 
 (*i*)
 open Term
@@ -137,6 +137,7 @@ exception FailError of int * Pp.std_ppcmds
    level or do nothing. *)
 val catch_failerror  : exn -> unit
 
+val tclORELSE0       : tactic -> tactic -> tactic
 val tclORELSE        : tactic -> tactic -> tactic
 val tclREPEAT        : tactic -> tactic
 val tclREPEAT_MAIN   : tactic -> tactic
diff --git a/proofs/tacexpr.ml b/proofs/tacexpr.ml
index 8e51171f..66136afa 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 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: tacexpr.ml 11739 2009-01-02 19:33:19Z herbelin $ i*)
 
 open Names
 open Topconstr
@@ -58,12 +58,7 @@ let make_red_flag =
   add_flag
     {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} 
 
-type hyp_location_flag = (* To distinguish body and type of local defs *)
-  | InHyp
-  | InHypTypeOnly
-  | InHypValueOnly
-
-type 'a raw_hyp_location = 'a with_occurrences * hyp_location_flag
+type 'a raw_hyp_location = 'a with_occurrences * Termops.hyp_location_flag
 
 type 'id move_location =
   | MoveAfter of 'id
@@ -103,7 +98,6 @@ type 'id message_token =
   | MsgInt of int
   | MsgIdent of 'id
 
-
 type 'id gsimple_clause = ('id raw_hyp_location) option
 (* onhyps:
      [None] means *on every hypothesis*
@@ -133,16 +127,15 @@ type multi =
   | RepeatStar
   | RepeatPlus
 
-type pattern_expr = constr_expr
-
 (* Type of patterns *)
 type 'a match_pattern =
   | Term of 'a
-  | Subterm of identifier option * 'a
+  | Subterm of bool * identifier option * 'a
 
 (* Type of hypotheses for a Match Context rule *)
 type 'a match_context_hyps =
   | Hyp of name located * 'a match_pattern
+  | Def of name located * 'a match_pattern * 'a match_pattern
 
 (* Type of a Match rule for Match Context and Match *)
 type ('a,'t) match_rule =
@@ -158,7 +151,8 @@ type ('constr,'pat,'cst,'ind,'ref,'id,'tac) gen_atomic_tactic_expr =
   | TacExact of 'constr
   | TacExactNoCheck of 'constr
   | TacVmCastNoCheck of 'constr
-  | TacApply of advanced_flag * evars_flag * 'constr with_bindings list
+  | TacApply of advanced_flag * evars_flag * 'constr with_bindings list * 
+      ('id * intro_pattern_expr located option) option
   | TacElim of evars_flag * 'constr with_bindings * 
       'constr with_bindings option
   | TacElimType of 'constr
@@ -170,7 +164,7 @@ 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 located * 'constr
+  | TacAssert of 'tac option * intro_pattern_expr located option * 'constr
   | TacGeneralize of ('constr with_occurrences * name) list
   | TacGeneralizeDep of 'constr
   | TacLetTac of name * 'constr * 'id gclause * letin_flag
@@ -287,7 +281,7 @@ and glob_tactic_expr =
 
 type raw_tactic_expr =
     (constr_expr,
-     pattern_expr,
+     constr_pattern_expr,
      reference or_by_notation,
      reference or_by_notation,
      reference,
@@ -296,7 +290,7 @@ type raw_tactic_expr =
 
 type raw_atomic_tactic_expr =
     (constr_expr,                  (* constr *)
-     pattern_expr,                 (* pattern *)
+     constr_pattern_expr,                 (* pattern *)
      reference or_by_notation,     (* evaluable reference *)
      reference or_by_notation,     (* inductive *)
      reference,                    (* ltac reference *)
@@ -305,7 +299,7 @@ type raw_atomic_tactic_expr =
 
 type raw_tactic_arg =
     (constr_expr,
-     pattern_expr,
+     constr_pattern_expr,
      reference or_by_notation,
      reference or_by_notation,
      reference,
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 6bbaff08..bf194d47 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(* $Id: tacmach.ml 11309 2008-08-06 10:30:35Z herbelin $ *)
+(* $Id: tacmach.ml 11639 2008-11-27 17:48:32Z barras $ *)
 
 open Pp
 open Util
@@ -202,6 +202,9 @@ 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 order_hyps idl gl =
+  refiner (Prim (Order idl)) gl
+
 let rec rename_hyp_no_check l gl = match l with 
   | [] -> tclIDTAC gl 
   | (id1,id2)::l -> 
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 2fc66e71..cdcb8bfd 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 11309 2008-08-06 10:30:35Z herbelin $ i*)
+(*i $Id: tacmach.mli 11639 2008-11-27 17:48:32Z barras $ i*)
 
 (*i*)
 open Names
@@ -133,6 +133,7 @@ val thin_body_no_check        : identifier list -> tactic
 val move_hyp_no_check         :
   bool -> identifier -> identifier move_location -> tactic
 val rename_hyp_no_check       : (identifier*identifier) list -> tactic
+val order_hyps : identifier list -> tactic
 val mutual_fix      :
   identifier -> int -> (identifier * int * constr) list -> tactic
 val mutual_cofix    : identifier -> (identifier * constr) list -> tactic
diff --git a/proofs/tactic_debug.ml b/proofs/tactic_debug.ml
index 2e19011f..7aa57d9b 100644
--- a/proofs/tactic_debug.ml
+++ b/proofs/tactic_debug.ml
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tactic_debug.ml 10739 2008-04-01 14:45:20Z herbelin $ i*)
+(*i $Id: tactic_debug.ml 11576 2008-11-10 19:13:15Z msozeau $ i*)
 
 open Names
 open Constrextern
@@ -129,7 +129,7 @@ let hyp_bound = function
   | Name id -> " (bound to "^(Names.string_of_id id)^")"
 
 (* Prints a matched hypothesis *)
-let db_matched_hyp debug env (id,c) ido =
+let db_matched_hyp debug env (id,_,c) ido =
   if debug <> DebugOff & !skip = 0 then
     msgnl (str "Hypothesis " ++
            str ((Names.string_of_id id)^(hyp_bound ido)^
@@ -148,8 +148,8 @@ let db_mc_pattern_success debug =
 
 let pp_match_pattern env = function
   | Term c -> Term (extern_constr_pattern (names_of_rel_context env) c)
-  | Subterm (o,c) ->
-    Subterm (o,(extern_constr_pattern (names_of_rel_context env) c))
+  | Subterm (b,o,c) ->
+    Subterm (b,o,(extern_constr_pattern (names_of_rel_context env) c))
 
 (* Prints a failure message for an hypothesis pattern *)
 let db_hyp_pattern_failure debug env (na,hyp) =
diff --git a/proofs/tactic_debug.mli b/proofs/tactic_debug.mli
index 6de8244d..63c89547 100644
--- a/proofs/tactic_debug.mli
+++ b/proofs/tactic_debug.mli
@@ -6,7 +6,7 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 
-(*i $Id: tactic_debug.mli 9092 2006-08-28 11:42:14Z bertot $ i*)
+(*i $Id: tactic_debug.mli 11576 2008-11-10 19:13:15Z msozeau $ i*)
 
 open Environ
 open Pattern
@@ -45,7 +45,7 @@ val db_pattern_rule :
 
 (* Prints a matched hypothesis *)
 val db_matched_hyp :
-  debug_info -> env -> identifier * constr -> name -> unit
+  debug_info -> env -> identifier * constr option * constr -> name -> unit
 
 (* Prints the matched conclusion *)
 val db_matched_concl : debug_info -> env -> constr -> unit