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

10 files changed, 69 insertions, 63 deletions

diff --git a/tactics/auto.ml b/tactics/auto.ml
index f4952cf0d2..4c00a60d00 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 73f8fde29b..55e23d342a 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 870e05e4b7..3b193f6d93 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 a14cf62870..2e7e9c3b2e 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 822198c7cc..3b734b4c64 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 95814302d9..a6915461d7 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 f0ca4ae506..41ed88d2f7 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 e2e6e3a71c..11625cbdff 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 f191bacf23..060cd94a87 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 a2dd6e4118..c52c145879 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