Moved allow_K to a unification flag

- seized the opportunity to align unification flags for functional induction to the ones of induction
- also tried to add delta in the elim_flags used in tactics.ml
- also tried to unify the rewrite flags in concl or in hyp (removed allow_K in hyps)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14186 85f007b7-540e-0410-9357-904b9bb8a0f7

17 files changed, 145 insertions, 106 deletions

diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml
index ad315035a..217a8fe4f 100644
--- a/plugins/decl_mode/decl_proof_instr.ml
+++ b/plugins/decl_mode/decl_proof_instr.ml
@@ -370,7 +370,7 @@ let find_subsubgoal c ctyp skip submetas gls =
     let se = Stack.pop stack in
       try
 	let unifier =
-	  Unification.w_unify true env Reduction.CUMUL
+	  Unification.w_unify env Reduction.CUMUL ~flags:Unification.elim_flags
 	    ctyp se.se_type se.se_evd in
 	  if n <= 0 then
 	      {se with
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 9e1ccd026..47fec1496 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -164,7 +164,8 @@ type unify_flags = {
   resolve_evars : bool;
   use_evars_pattern_unification : bool;
   modulo_betaiota : bool;
-  modulo_eta : bool
+  modulo_eta : bool;
+  allow_K_in_toplevel_higher_order_unification : bool
 }
 
 let default_unify_flags = {
@@ -175,7 +176,8 @@ let default_unify_flags = {
   resolve_evars = false;
   use_evars_pattern_unification = true;
   modulo_betaiota = false;
-  modulo_eta = true
+  modulo_eta = true;
+  allow_K_in_toplevel_higher_order_unification = false
 }
 
 let default_no_delta_unify_flags = {
@@ -186,7 +188,32 @@ let default_no_delta_unify_flags = {
   resolve_evars = false;
   use_evars_pattern_unification = false;
   modulo_betaiota = false;
-  modulo_eta = true
+  modulo_eta = true;
+  allow_K_in_toplevel_higher_order_unification = false
+}
+
+let elim_flags = {
+  modulo_conv_on_closed_terms = Some full_transparent_state;
+  use_metas_eagerly = true;
+  modulo_delta = full_transparent_state;
+  modulo_delta_types = full_transparent_state;
+  resolve_evars = false;
+  use_evars_pattern_unification = true;
+  modulo_betaiota = false;
+  modulo_eta = true;
+  allow_K_in_toplevel_higher_order_unification = true
+}
+
+let elim_no_delta_flags = {
+  modulo_conv_on_closed_terms = Some full_transparent_state;
+  use_metas_eagerly = true;
+  modulo_delta = empty_transparent_state;
+  modulo_delta_types = full_transparent_state;
+  resolve_evars = false;
+  use_evars_pattern_unification = false;
+  modulo_betaiota = false;
+  modulo_eta = true;
+  allow_K_in_toplevel_higher_order_unification = true
 }
 
 let use_evars_pattern_unification flags =
@@ -936,25 +963,28 @@ let w_unify_to_subterm_all env ?(flags=default_unify_flags) (op,cl) evd =
   else
     res
 
-let w_unify_to_subterm_list env flags allow_K hdmeta oplist t evd =
+let w_unify_to_subterm_list env flags hdmeta oplist t evd =
   List.fold_right
     (fun op (evd,l) ->
       let op = whd_meta evd op in
       if isMeta op then
-	if allow_K then (evd,op::l)
+	if flags.allow_K_in_toplevel_higher_order_unification then (evd,op::l)
 	else error_abstraction_over_meta env evd hdmeta (destMeta op)
       else if occur_meta_or_existential op then
         let (evd',cl) =
           try
 	    (* This is up to delta for subterms w/o metas ... *)
 	    w_unify_to_subterm env ~flags (strip_outer_cast op,t) evd
-	  with PretypeError (env,_,NoOccurrenceFound _) when allow_K -> (evd,op)
+	  with PretypeError (env,_,NoOccurrenceFound _) when
+              flags.allow_K_in_toplevel_higher_order_unification -> (evd,op)
         in
-	  if not allow_K && (* ensure we found a different instance *)
+	  if not flags.allow_K_in_toplevel_higher_order_unification &&
+            (* ensure we found a different instance *)
 	    List.exists (fun op -> eq_constr op cl) l
 	  then error_non_linear_unification env evd hdmeta cl
 	  else (evd',cl::l)
-      else if allow_K or dependent op t then
+      else if flags.allow_K_in_toplevel_higher_order_unification or dependent op t
+      then
 	(evd,op::l)
       else
 	(* This is not up to delta ... *)
@@ -962,29 +992,28 @@ let w_unify_to_subterm_list env flags allow_K hdmeta oplist t evd =
     oplist
     (evd,[])
 
-let secondOrderAbstraction env flags allow_K typ (p, oplist) evd =
+let secondOrderAbstraction env flags typ (p, oplist) evd =
   (* Remove delta when looking for a subterm *)
   let flags = { flags with modulo_delta = (fst flags.modulo_delta, Cpred.empty) } in
-  let (evd',cllist) =
-    w_unify_to_subterm_list env flags allow_K p oplist typ evd in
+  let (evd',cllist) = w_unify_to_subterm_list env flags p oplist typ evd in
   let typp = Typing.meta_type evd' p in
   let pred = abstract_list_all env evd' typp typ cllist in
   w_merge env false flags (evd',[p,pred,(Conv,TypeProcessed)],[])
 
-let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
+let w_unify2 env flags cv_pb ty1 ty2 evd =
   let c1, oplist1 = whd_stack evd ty1 in
   let c2, oplist2 = whd_stack evd ty2 in
   match kind_of_term c1, kind_of_term c2 with
     | Meta p1, _ ->
         (* Find the predicate *)
 	let evd' =
-          secondOrderAbstraction env flags allow_K ty2 (p1,oplist1) evd in
+          secondOrderAbstraction env flags ty2 (p1,oplist1) evd in
         (* Resume first order unification *)
 	w_unify_0 env cv_pb flags (nf_meta evd' ty1) ty2 evd'
     | _, Meta p2 ->
         (* Find the predicate *)
 	let evd' =
-          secondOrderAbstraction env flags allow_K ty1 (p2, oplist2) evd in
+          secondOrderAbstraction env flags ty1 (p2, oplist2) evd in
         (* Resume first order unification *)
 	w_unify_0 env cv_pb flags ty1 (nf_meta evd' ty2) evd'
     | _ -> error "w_unify2"
@@ -1009,7 +1038,7 @@ let w_unify2 env flags allow_K cv_pb ty1 ty2 evd =
    Before, second-order was used if the type of Meta(1) and [x:A]t was
    convertible and first-order otherwise. But if failed if e.g. the type of
    Meta(1) had meta-variables in it. *)
-let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
+let w_unify env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
   let hd1,l1 = whd_stack evd ty1 in
   let hd2,l2 = whd_stack evd ty2 in
     match kind_of_term hd1, l1<>[], kind_of_term hd2, l2<>[] with
@@ -1020,13 +1049,13 @@ let w_unify allow_K env cv_pb ?(flags=default_unify_flags) ty1 ty2 evd =
 	      w_typed_unify env cv_pb flags ty1 ty2 evd
 	    with ex when precatchable_exception ex ->
 	      try
-		w_unify2 env flags allow_K cv_pb ty1 ty2 evd
+		w_unify2 env flags cv_pb ty1 ty2 evd
 	      with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e)
 
       (* Second order case *)
       | (Meta _, true, _, _ | _, _, Meta _, true) ->
 	  (try
-	      w_unify2 env flags allow_K cv_pb ty1 ty2 evd
+	      w_unify2 env flags cv_pb ty1 ty2 evd
 	    with PretypeError (env,_,NoOccurrenceFound _) as e -> raise e
 	      | ex when precatchable_exception ex ->
 		  try
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index cd8e70418..0f7eec692 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -18,15 +18,19 @@ type unify_flags = {
   resolve_evars : bool;
   use_evars_pattern_unification : bool;
   modulo_betaiota : bool;
-  modulo_eta : bool
+  modulo_eta : bool;
+  allow_K_in_toplevel_higher_order_unification : bool
 }
 
 val default_unify_flags : unify_flags
 val default_no_delta_unify_flags : unify_flags
 
+val elim_flags : unify_flags
+val elim_no_delta_flags : unify_flags
+
 (** The "unique" unification fonction *)
 val w_unify :
-  bool -> env -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map -> evar_map
+  env -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map -> evar_map
 
 (** [w_unify_to_subterm env (c,t) m] performs unification of [c] with a
    subterm of [t]. Constraints are added to [m] and the matched
diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 632bf3a62..35552b8d8 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -265,20 +265,20 @@ let clenv_dependent ce = clenv_dependent_gen false ce
 
 (******************************************************************)
 
-let clenv_unify allow_K ?(flags=default_unify_flags) cv_pb t1 t2 clenv =
+let clenv_unify ?(flags=default_unify_flags) cv_pb t1 t2 clenv =
   { clenv with
-      evd = w_unify allow_K ~flags:flags clenv.env cv_pb t1 t2 clenv.evd }
+      evd = w_unify ~flags clenv.env cv_pb t1 t2 clenv.evd }
 
 let clenv_unify_meta_types ?(flags=default_unify_flags) clenv =
   { clenv with evd = w_unify_meta_types ~flags:flags clenv.env clenv.evd }
 
-let clenv_unique_resolver allow_K ?(flags=default_unify_flags) clenv gl =
+let clenv_unique_resolver ?(flags=default_unify_flags) clenv gl =
   let concl = Goal.V82.concl clenv.evd (sig_it gl) in
   if isMeta (fst (whd_stack clenv.evd clenv.templtyp.rebus)) then
-    clenv_unify allow_K CUMUL ~flags:flags (clenv_type clenv) concl
-      (clenv_unify_meta_types ~flags:flags clenv)
+    clenv_unify CUMUL ~flags (clenv_type clenv) concl
+      (clenv_unify_meta_types ~flags clenv)
   else
-    clenv_unify allow_K CUMUL ~flags:flags
+    clenv_unify CUMUL ~flags
       (meta_reducible_instance clenv.evd clenv.templtyp) concl clenv
 
 (* [clenv_pose_metas_as_evars clenv dep_mvs]
@@ -356,7 +356,7 @@ let connect_clenv gls clenv =
 
    In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma].
 *)
-let clenv_fchain ?(allow_K=true) ?(flags=default_unify_flags) mv clenv nextclenv =
+let clenv_fchain ?(flags=elim_flags) mv clenv nextclenv =
   (* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
   let clenv' =
     { templval = clenv.templval;
@@ -365,7 +365,7 @@ let clenv_fchain ?(allow_K=true) ?(flags=default_unify_flags) mv clenv nextclenv
       env = nextclenv.env } in
   (* unify the type of the template of [nextclenv] with the type of [mv] *)
   let clenv'' =
-    clenv_unify allow_K ~flags:flags CUMUL
+    clenv_unify ~flags:flags CUMUL
       (clenv_term clenv' nextclenv.templtyp)
       (clenv_meta_type clenv' mv)
       clenv' in
diff --git a/proofs/clenv.mli b/proofs/clenv.mli
index af51e6716..b685f5041 100644
--- a/proofs/clenv.mli
+++ b/proofs/clenv.mli
@@ -54,22 +54,22 @@ val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> claus
 
 val connect_clenv : Goal.goal sigma -> clausenv -> clausenv
 val clenv_fchain :
-  ?allow_K:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
+  ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
 
 (** {6 Unification with clenvs } *)
 
 (** Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *)
 val clenv_unify :
-  bool -> ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
+  ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
 
 (** unifies the concl of the goal with the type of the clenv *)
 val clenv_unique_resolver :
-  bool -> ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
+  ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
 
 (** same as above ([allow_K=false]) but replaces remaining metas
    with fresh evars if [evars_flag] is [true] *)
 val evar_clenv_unique_resolver :
-  bool -> ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
+  ?flags:unify_flags -> clausenv -> Goal.goal sigma -> clausenv
 
 val clenv_dependent : clausenv -> metavariable list
 
diff --git a/proofs/clenvtac.ml b/proofs/clenvtac.ml
index e4ad27f2e..e05651952 100644
--- a/proofs/clenvtac.ml
+++ b/proofs/clenvtac.ml
@@ -81,17 +81,18 @@ let clenv_refine with_evars ?(with_classes=true) clenv gls =
     (refine (clenv_cast_meta clenv (clenv_value clenv)))
     gls
 
-let dft = Unification.default_unify_flags
+open Unification
+
+let dft = default_unify_flags
 
-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 res_pf clenv ?(with_evars=false) ?(flags=dft) gls =
+  clenv_refine with_evars (clenv_unique_resolver ~flags clenv gls) gls
 
 let elim_res_pf_THEN_i clenv tac gls =
-  let clenv' = (clenv_unique_resolver true clenv gls) in
+  let clenv' = (clenv_unique_resolver ~flags:elim_flags clenv gls) in
   tclTHENLASTn (clenv_refine false clenv') (tac clenv') gls
 
-let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft
+let e_res_pf clenv = res_pf clenv ~with_evars:true ~flags:dft
 
 
 (* [unifyTerms] et [unify] ne semble pas gérer les Meta, en
@@ -99,8 +100,6 @@ let e_res_pf clenv = res_pf clenv ~with_evars:true ~allow_K:false ~flags:dft
    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;
@@ -109,14 +108,15 @@ let fail_quick_unif_flags = {
   resolve_evars = false;
   use_evars_pattern_unification = false;
   modulo_betaiota = false;
-  modulo_eta = true
+  modulo_eta = true;
+  allow_K_in_toplevel_higher_order_unification = false
 }
 
 (* let unifyTerms m n = walking (fun wc -> fst (w_Unify CONV m n [] wc)) *)
 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 m n evd in
+  let evd' = w_unify env CONV ~flags m n evd in
   tclIDTAC {it = gls.it; sigma =  evd'}
 
 let unify ?(flags=fail_quick_unif_flags) m gls =
diff --git a/proofs/clenvtac.mli b/proofs/clenvtac.mli
index d288eddd2..49a961f5d 100644
--- a/proofs/clenvtac.mli
+++ b/proofs/clenvtac.mli
@@ -19,7 +19,7 @@ open Unification
 (** Tactics *)
 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 res_pf : clausenv -> ?with_evars:evars_flag -> ?flags:unify_flags -> tactic
 val elim_res_pf_THEN_i : clausenv -> (clausenv -> tactic array) -> tactic
 
 val clenv_pose_dependent_evars : evars_flag -> clausenv -> clausenv
diff --git a/tactics/auto.ml b/tactics/auto.ml
index f4952cf0d..4c00a60d0 100644
--- a/tactics/auto.ml
+++ b/tactics/auto.ml
@@ -846,7 +846,8 @@ let auto_unif_flags = {
   resolve_evars = true;
   use_evars_pattern_unification = false;
   modulo_betaiota = false;
-  modulo_eta = true
+  modulo_eta = true;
+  allow_K_in_toplevel_higher_order_unification = false
 }
 
 (* Try unification with the precompiled clause, then use registered Apply *)
@@ -857,12 +858,12 @@ let h_clenv_refine ev c clenv =
 
 let unify_resolve_nodelta (c,clenv) gl =
   let clenv' = connect_clenv gl clenv in
-  let clenv'' = clenv_unique_resolver false ~flags:auto_unif_flags clenv' gl in
+  let clenv'' = clenv_unique_resolver ~flags:auto_unif_flags clenv' gl in
   h_clenv_refine false c clenv'' gl
 
 let unify_resolve flags (c,clenv) gl =
   let clenv' = connect_clenv gl clenv in
-  let clenv'' = clenv_unique_resolver false ~flags clenv' gl in
+  let clenv'' = clenv_unique_resolver ~flags clenv' gl in
   h_clenv_refine false c clenv'' gl
 
 let unify_resolve_gen = function
diff --git a/tactics/autorewrite.ml b/tactics/autorewrite.ml
index 73f8fde29..55e23d342 100644
--- a/tactics/autorewrite.ml
+++ b/tactics/autorewrite.ml
@@ -246,7 +246,7 @@ type hypinfo = {
 
 let evd_convertible env evd x y =
   try
-    ignore(Unification.w_unify true env Reduction.CONV x y evd); true 
+    ignore(Unification.w_unify ~flags:Unification.elim_flags env Reduction.CONV x y evd); true 
   (* try ignore(Evarconv.the_conv_x env x y evd); true *)
   with _ -> false
 
diff --git a/tactics/class_tactics.ml4 b/tactics/class_tactics.ml4
index 870e05e4b..3b193f6d9 100644
--- a/tactics/class_tactics.ml4
+++ b/tactics/class_tactics.ml4
@@ -80,7 +80,8 @@ let auto_unif_flags = {
   resolve_evars = false;
   use_evars_pattern_unification = true;
   modulo_betaiota = true;
-  modulo_eta = true
+  modulo_eta = true;
+  allow_K_in_toplevel_higher_order_unification = false
 }
 
 let rec eq_constr_mod_evars x y =
@@ -103,12 +104,12 @@ END
 
 let unify_e_resolve flags (c,clenv) gls =
   let clenv' = connect_clenv gls clenv in
-  let clenv' = clenv_unique_resolver false ~flags clenv' gls in
+  let clenv' = clenv_unique_resolver ~flags clenv' gls in
     Clenvtac.clenv_refine true ~with_classes:false clenv' gls
 
 let unify_resolve flags (c,clenv) gls =
   let clenv' = connect_clenv gls clenv in
-  let clenv' = clenv_unique_resolver false ~flags clenv' gls in
+  let clenv' = clenv_unique_resolver ~flags clenv' gls in
     Clenvtac.clenv_refine false ~with_classes:false clenv' gls
 
 let clenv_of_prods nprods (c, clenv) gls =
diff --git a/tactics/eauto.ml4 b/tactics/eauto.ml4
index a14cf6287..2e7e9c3b2 100644
--- a/tactics/eauto.ml4
+++ b/tactics/eauto.ml4
@@ -93,7 +93,7 @@ let priority l = List.map snd (List.filter (fun (pr,_) -> pr = 0) l)
 
 let unify_e_resolve flags (c,clenv) gls =
   let clenv' = connect_clenv gls clenv in
-  let _ = clenv_unique_resolver false ~flags clenv' gls in
+  let _ = clenv_unique_resolver ~flags clenv' gls in
   h_simplest_eapply c gls
 
 let rec e_trivial_fail_db db_list local_db goal =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index 822198c7c..3b734b4c6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -88,7 +88,9 @@ let rewrite_unif_flags = {
   Unification.resolve_evars = true;
   Unification.use_evars_pattern_unification = true;
   Unification.modulo_betaiota = false;
-  Unification.modulo_eta = true
+  Unification.modulo_eta = true;
+  Unification.allow_K_in_toplevel_higher_order_unification = false
+    (* allow_K does not matter in practice because calls w_typed_unify *)
 }
 
 let side_tac tac sidetac =
@@ -120,11 +122,27 @@ let instantiate_lemma env sigma gl c ty l l2r concl =
   let eqclause = Clenv.make_clenv_binding gl (c,t) l in
    [eqclause]
 
-let rewrite_elim with_evars c e ?(allow_K=true) =
-  general_elim_clause_gen (elimination_clause_scheme with_evars allow_K) c e
+let rewrite_conv_closed_unif_flags = {
+  Unification.modulo_conv_on_closed_terms = Some full_transparent_state;
+  Unification.use_metas_eagerly = true;
+  Unification.modulo_delta = empty_transparent_state;
+  Unification.modulo_delta_types = full_transparent_state;
+  Unification.resolve_evars = false;
+  Unification.use_evars_pattern_unification = true;
+  Unification.modulo_betaiota = false;
+  Unification.modulo_eta = true;
+  Unification.allow_K_in_toplevel_higher_order_unification = false
+}
+
+let rewrite_elim with_evars c e =
+  general_elim_clause_gen
+    (elimination_clause_scheme with_evars ~flags:rewrite_conv_closed_unif_flags)
+     c e
 
 let rewrite_elim_in with_evars id c e =
-  general_elim_clause_gen (elimination_in_clause_scheme with_evars id) c e
+  general_elim_clause_gen
+    (elimination_in_clause_scheme with_evars
+       ~flags:rewrite_conv_closed_unif_flags id) c e
 
 (* Ad hoc asymmetric general_elim_clause *)
 let general_elim_clause with_evars cls rew elim =
@@ -134,7 +152,7 @@ let general_elim_clause with_evars cls rew elim =
 	  (* was tclWEAK_PROGRESS which only fails for tactics generating one
              subgoal and did not fail for useless conditional rewritings generating
              an extra condition *)
-	  tclNOTSAMEGOAL (rewrite_elim with_evars rew elim ~allow_K:false)
+	  tclNOTSAMEGOAL (rewrite_elim with_evars rew elim)
       | Some id -> rewrite_elim_in with_evars id rew elim)
   with Pretype_errors.PretypeError (env,evd,
 				    Pretype_errors.NoOccurrenceFound (c', _)) ->
diff --git a/tactics/leminv.ml b/tactics/leminv.ml
index 95814302d..a6915461d 100644
--- a/tactics/leminv.ml
+++ b/tactics/leminv.ml
@@ -271,7 +271,7 @@ let lemInv id c gls =
   try
     let clause = mk_clenv_type_of gls c in
     let clause = clenv_constrain_last_binding (mkVar id) clause in
-    Clenvtac.res_pf clause ~allow_K:true gls
+    Clenvtac.res_pf clause ~flags:Unification.elim_flags gls
   with
     | NoSuchBinding ->
 	errorlabstrm ""
diff --git a/tactics/rewrite.ml4 b/tactics/rewrite.ml4
index f0ca4ae50..41ed88d2f 100644
--- a/tactics/rewrite.ml4
+++ b/tactics/rewrite.ml4
@@ -308,7 +308,8 @@ let rewrite_unif_flags = {
   Unification.resolve_evars = true;
   Unification.use_evars_pattern_unification = true;
   Unification.modulo_betaiota = false;
-  Unification.modulo_eta = true
+  Unification.modulo_eta = true;
+  Unification.allow_K_in_toplevel_higher_order_unification = true
 }
 
 let rewrite2_unif_flags = 
@@ -319,7 +320,8 @@ let rewrite2_unif_flags =
      Unification.resolve_evars = true;
      Unification.use_evars_pattern_unification = true;
      Unification.modulo_betaiota = true;
-     Unification.modulo_eta = true
+     Unification.modulo_eta = true;
+     Unification.allow_K_in_toplevel_higher_order_unification = true
   }
 
 let general_rewrite_unif_flags () = 
@@ -331,13 +333,12 @@ let general_rewrite_unif_flags () =
        Unification.resolve_evars = true;
        Unification.use_evars_pattern_unification = true;
        Unification.modulo_betaiota = true;
-       Unification.modulo_eta = true }
+       Unification.modulo_eta = true;
+       Unification.allow_K_in_toplevel_higher_order_unification = true }
 
 let convertible env evd x y =
   Reductionops.is_conv env evd x y
 
-let allowK = true
-
 let refresh_hypinfo env sigma hypinfo =
   if hypinfo.abs = None then
     let {l2r=l2r; c=c;cl=cl;flags=flags} = hypinfo in
@@ -356,11 +357,10 @@ let unify_eqn env sigma hypinfo t =
     let env', prf, c1, c2, car, rel =
       match abs with
       | Some (absprf, absprfty) ->
-	  let env' = clenv_unify allowK ~flags:rewrite_unif_flags CONV left t cl in
+	  let env' = clenv_unify ~flags:rewrite_unif_flags CONV left t cl in
 	    env', prf, c1, c2, car, rel
       | None ->
-	  let env' =
-	    clenv_unify allowK ~flags:!hypinfo.flags CONV left t cl
+	  let env' = clenv_unify ~flags:!hypinfo.flags CONV left t cl
 	  in
 	  let env' = Clenvtac.clenv_pose_dependent_evars true env' in
 (* 	  let env' = Clenv.clenv_pose_metas_as_evars env' (Evd.undefined_metas env'.evd) in *)
@@ -1018,7 +1018,7 @@ module Strategies =
 	  with _ -> error "fold: the term is not unfoldable !"
 	in
 	  try
-	    let sigma = Unification.w_unify true env CONV ~flags:Unification.default_unify_flags unfolded t sigma in
+	    let sigma = Unification.w_unify env CONV ~flags:Unification.elim_flags unfolded t sigma in
 	    let c' = Evarutil.nf_evar sigma c in
 	      Some (Some { rew_car = ty; rew_from = t; rew_to = c';
 			   rew_prf = RewCast DEFAULTcast; 
diff --git a/tactics/tacticals.ml b/tactics/tacticals.ml
index e2e6e3a71..11625cbdf 100644
--- a/tactics/tacticals.ml
+++ b/tactics/tacticals.ml
@@ -363,7 +363,8 @@ let general_elim_then_using mk_elim
     match predicate with
        | None   -> elimclause'
        | Some p ->
-           clenv_unify true Reduction.CONV (mkMeta pmv) p elimclause'
+           clenv_unify ~flags:Unification.elim_flags
+             Reduction.CONV (mkMeta pmv) p elimclause'
   in
   elim_res_pf_THEN_i elimclause' branchtacs gl
 
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index f191bacf2..060cd94a8 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -704,27 +704,15 @@ let index_of_ind_arg t =
       | None -> error "Could not find inductive argument of elimination scheme."
   in aux None 0 t
 
-let elim_flags = {
-  modulo_conv_on_closed_terms = Some full_transparent_state;
-  use_metas_eagerly = true;
-  modulo_delta = empty_transparent_state;
-  modulo_delta_types = full_transparent_state;
-  resolve_evars = false;
-  use_evars_pattern_unification = true;
-  modulo_betaiota = false;
-  modulo_eta = true
-}
-
-let elimination_clause_scheme with_evars allow_K i elimclause indclause gl =
+let elimination_clause_scheme with_evars ?(flags=elim_flags) i elimclause indclause gl =
   let indmv =
     (match kind_of_term (nth_arg i elimclause.templval.rebus) with
        | Meta mv -> mv
        | _  -> errorlabstrm "elimination_clause"
              (str "The type of elimination clause is not well-formed."))
   in
-  let elimclause' = clenv_fchain ~flags:elim_flags indmv elimclause indclause in
-  res_pf elimclause' ~with_evars:with_evars ~allow_K:allow_K ~flags:elim_flags
-    gl
+  let elimclause' = clenv_fchain ~flags indmv elimclause indclause in
+  res_pf elimclause' ~with_evars:with_evars ~flags gl
 
 (*
  * Elimination tactic with bindings and using an arbitrary
@@ -753,8 +741,8 @@ let general_elim_clause elimtac (c,lbindc) elim gl =
   let indclause  = make_clenv_binding gl (c,t) lbindc  in
     general_elim_clause_gen elimtac indclause elim gl
 
-let general_elim with_evars c e ?(allow_K=true) =
-  general_elim_clause (elimination_clause_scheme with_evars allow_K) c e
+let general_elim with_evars c e =
+  general_elim_clause (elimination_clause_scheme with_evars) c e
 
 (* Elimination tactic with bindings but using the default elimination
  * constant associated with the type. *)
@@ -770,7 +758,6 @@ let default_elim with_evars (c,_ as cx) gl =
 let elim_in_context with_evars c = function
   | Some elim ->
       general_elim with_evars c {elimindex = Some (-1); elimbody = elim}
-	~allow_K:true
   | None -> default_elim with_evars c
 
 let elim with_evars (c,lbindc as cx) elim =
@@ -795,13 +782,13 @@ let simplest_elim c = default_elim false (c,NoBindings)
    (e.g. it could replace id:A->B->C by id:C, knowing A/\B)
 *)
 
-let clenv_fchain_in id elim_flags mv elimclause hypclause =
-  try clenv_fchain ~allow_K:false ~flags:elim_flags mv elimclause hypclause
+let clenv_fchain_in id ?(flags=elim_flags) mv elimclause hypclause =
+  try clenv_fchain ~flags mv elimclause hypclause
   with PretypeError (env,evd,NoOccurrenceFound (op,_)) ->
     (* Set the hypothesis name in the message *)
     raise (PretypeError (env,evd,NoOccurrenceFound (op,Some id)))
 
-let elimination_in_clause_scheme with_evars id i elimclause indclause gl =
+let elimination_in_clause_scheme with_evars ?(flags=elim_flags) id i elimclause indclause gl =
   let indmv = destMeta (nth_arg i elimclause.templval.rebus) in
   let hypmv =
     try match list_remove indmv (clenv_independent elimclause) with
@@ -809,12 +796,11 @@ let elimination_in_clause_scheme with_evars id i elimclause indclause gl =
       | _ -> failwith ""
     with Failure _ -> errorlabstrm "elimination_clause"
           (str "The type of elimination clause is not well-formed.") in
-  let elimclause'  = clenv_fchain indmv elimclause indclause in
+  let elimclause'  = clenv_fchain ~flags indmv elimclause indclause in
   let hyp = mkVar id in
   let hyp_typ = pf_type_of gl hyp in
   let hypclause = mk_clenv_from_n gl (Some 0) (hyp, hyp_typ) in
-  let elimclause'' =
-    clenv_fchain_in id elim_flags hypmv elimclause' hypclause in
+  let elimclause'' = clenv_fchain_in id ~flags hypmv elimclause' hypclause in
   let new_hyp_typ  = clenv_type elimclause'' in
   if eq_constr hyp_typ new_hyp_typ then
     errorlabstrm "general_rewrite_in"
@@ -1008,8 +994,7 @@ let apply_in_once_main flags innerclause (d,lbind) gl =
 
 let apply_in_once sidecond_first with_delta with_destruct with_evars id
   (loc,(d,lbind)) gl0 =
-  let flags =
-    if with_delta then default_unify_flags else default_no_delta_unify_flags in
+  let flags = if with_delta then elim_flags else elim_no_delta_flags in
   let t' = pf_get_hyp_typ gl0 id in
   let innerclause = mk_clenv_from_n gl0 (Some 0) (mkVar id,t') in
   let rec aux with_destruct c gl =
@@ -2857,7 +2842,7 @@ let induction_tac_felim with_evars indvars nparams elim gl =
   (* elimclause' is built from elimclause by instanciating all args and params. *)
   let elimclause' = recolle_clenv nparams indvars elimclause gl in
   (* one last resolution (useless?) *)
-  let resolved = clenv_unique_resolver true elimclause' gl in
+  let resolved = clenv_unique_resolver ~flags:elim_flags elimclause' gl in
   clenv_refine with_evars resolved gl
 
 (* Apply induction "in place" replacing the hypothesis on which
@@ -2953,7 +2938,7 @@ let induction_tac with_evars elim (varname,lbind) typ gl =
   let elimclause =
     make_clenv_binding gl
       (mkCast (elimc,DEFAULTcast,elimt),elimt) lbindelimc in
-  elimination_clause_scheme with_evars true i elimclause indclause gl
+  elimination_clause_scheme with_evars i elimclause indclause gl
 
 let induction_from_context isrec with_evars (indref,nparams,elim) (hyp0,lbind) names
   inhyps gl =
@@ -3176,9 +3161,9 @@ let elim_scheme_type elim t gl =
     | Meta mv ->
         let clause' =
 	  (* t is inductive, then CUMUL or CONV is irrelevant *)
-	  clenv_unify true Reduction.CUMUL t
+	  clenv_unify ~flags:elim_flags Reduction.CUMUL t
             (clenv_meta_type clause mv) clause in
-	res_pf clause' ~allow_K:true gl
+	res_pf clause' ~flags:elim_flags gl
     | _ -> anomaly "elim_scheme_type"
 
 let elim_type t gl =
@@ -3480,7 +3465,6 @@ let unify ?(state=full_transparent_state) x y gl =
 	modulo_delta = state;
 	modulo_conv_on_closed_terms = Some state}
     in
-    let evd = w_unify false (pf_env gl) Reduction.CONV
-      ~flags x y (project gl)
+    let evd = w_unify (pf_env gl) Reduction.CONV ~flags x y (project gl)
     in tclEVARS evd gl
   with _ -> tclFAIL 0 (str"Not unifiable") gl
diff --git a/tactics/tactics.mli b/tactics/tactics.mli
index a2dd6e411..c52c14587 100644
--- a/tactics/tactics.mli
+++ b/tactics/tactics.mli
@@ -26,6 +26,7 @@ open Nametab
 open Glob_term
 open Pattern
 open Termops
+open Unification
 
 (** Main tactics. *)
 
@@ -248,19 +249,19 @@ type eliminator = {
   elimbody : constr with_bindings
 }
 
-val elimination_clause_scheme : evars_flag ->
-  bool -> int -> clausenv -> clausenv -> tactic
+val elimination_clause_scheme : evars_flag -> ?flags:unify_flags -> 
+  int -> clausenv -> clausenv -> tactic
 
-val elimination_in_clause_scheme : evars_flag -> identifier -> int ->
-  clausenv -> clausenv -> tactic
+val elimination_in_clause_scheme : evars_flag -> ?flags:unify_flags -> 
+  identifier -> int -> clausenv -> clausenv -> tactic
 
 val general_elim_clause_gen : (int -> Clenv.clausenv -> 'a -> tactic) ->
   'a -> eliminator -> tactic
 
 val general_elim  : evars_flag ->
-  constr with_bindings -> eliminator -> ?allow_K:bool -> tactic
-val general_elim_in : evars_flag ->
-  identifier -> constr with_bindings -> eliminator -> tactic
+  constr with_bindings -> eliminator -> tactic
+val general_elim_in : evars_flag -> identifier ->
+  constr with_bindings -> eliminator -> tactic
 
 val default_elim  : evars_flag -> constr with_bindings -> tactic
 val simplest_elim : constr -> tactic