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

4 files changed, 23 insertions, 23 deletions

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