Passing around the flag for injection so that tactics calling inj at

ML level can set the flags themselves.

In particular, using injection and discriminate with option "Keep
Proofs Equalities" when called from "decide equality" and "Scheme
Equality".

This fixes bug #5281.

4 files changed, 78 insertions, 49 deletions

diff --git a/tactics/eqdecide.ml b/tactics/eqdecide.ml
index d912decff..8764ef085 100644
--- a/tactics/eqdecide.ml
+++ b/tactics/eqdecide.ml
@@ -89,6 +89,12 @@ let mkBranches (eqonleft,mk,c1,c2,typ) =
      clear_last;
      intros]
 
+let inj_flags = Some {
+    Equality.keep_proof_equalities = true; (* necessary *)
+    Equality.injection_in_context = true; (* does not matter here *)
+    Equality.injection_pattern_l2r_order = true; (* does not matter here *)
+  }
+
 let discrHyp id =
   let c env sigma = (sigma, (mkVar id, NoBindings)) in
   let tac c = Equality.discr_tac false (Some (None, ElimOnConstr c)) in
@@ -136,7 +142,7 @@ let eqCase tac =
 
 let injHyp id =
   let c env sigma = (sigma, (mkVar id, NoBindings)) in
-  let tac c = Equality.injClause None false (Some (None, ElimOnConstr c)) in
+  let tac c = Equality.injClause inj_flags None false (Some (None, ElimOnConstr c)) in
   Tacticals.New.tclDELAYEDWITHHOLES false c tac
 
 let diseqCase hyps eqonleft =
diff --git a/tactics/equality.ml b/tactics/equality.ml
index bb2de1904..7c03a3ba6 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -48,6 +48,12 @@ module NamedDecl = Context.Named.Declaration
 
 (* Options *)
 
+type inj_flags = {
+    keep_proof_equalities : bool;
+    injection_in_context : bool;
+    injection_pattern_l2r_order : bool;
+  }
+
 let discriminate_introduction = ref true
 
 let discr_do_intro () = !discriminate_introduction
@@ -63,7 +69,9 @@ let _ =
 
 let injection_pattern_l2r_order = ref true
 
-let use_injection_pattern_l2r_order () = !injection_pattern_l2r_order
+let use_injection_pattern_l2r_order = function
+  | None -> !injection_pattern_l2r_order
+  | Some flags -> flags.injection_pattern_l2r_order
 
 let _ =
   declare_bool_option
@@ -75,9 +83,9 @@ let _ =
 
 let injection_in_context = ref false
 
-let use_injection_in_context () =
-  !injection_in_context
-  && Flags.version_strictly_greater Flags.V8_5
+let use_injection_in_context = function
+  | None -> !injection_in_context && Flags.version_strictly_greater Flags.V8_5
+  | Some flags -> flags.injection_in_context
 
 let _ =
   declare_bool_option
@@ -721,7 +729,14 @@ let _ =
       optread  = (fun () -> !keep_proof_equalities_for_injection) ;
       optwrite = (fun b -> keep_proof_equalities_for_injection := b) }
 
-let find_positions env sigma ~no_discr t1 t2 =
+let keep_proof_equalities = function
+  | None -> !keep_proof_equalities_for_injection
+  | Some flags -> flags.keep_proof_equalities
+
+(* [keep_proofs] is relevant for types in Prop with elimination in Type *)
+(* In particular, it is relevant for injection but not for discriminate *)
+
+let find_positions env sigma ~keep_proofs ~no_discr t1 t2 =
   let project env sorts posn t1 t2 =
     let ty1 = get_type_of env sigma t1 in
     let s = get_sort_family_of env sigma ty1 in
@@ -768,20 +783,22 @@ let find_positions env sigma ~no_discr t1 t2 =
 	    project env sorts posn t1_0 t2_0
   in
   try
-    let sorts = if !keep_proof_equalities_for_injection then [InSet;InType;InProp]
-		else [InSet;InType]
-    in
+    let sorts = if keep_proofs then [InSet;InType;InProp] else [InSet;InType] in
     Inr (findrec sorts [] t1 t2)
   with DiscrFound (path,c1,c2) ->
     Inl (path,c1,c2)
 
+let use_keep_proofs = function
+  | None -> !keep_proof_equalities_for_injection
+  | Some b -> b
+
 let discriminable env sigma t1 t2 =
-  match find_positions env sigma ~no_discr:false t1 t2 with
+  match find_positions env sigma ~keep_proofs:false ~no_discr:false t1 t2 with
     | Inl _ -> true
     | _ -> false
 
-let injectable env sigma t1 t2 =
-    match find_positions env sigma ~no_discr:true t1 t2 with
+let injectable env sigma ~keep_proofs t1 t2 =
+    match find_positions env sigma ~keep_proofs:(use_keep_proofs keep_proofs) ~no_discr:true t1 t2 with
     | Inl _ -> assert false
     | Inr [] | Inr [([],_,_)] -> false
     | Inr _ -> true
@@ -1024,7 +1041,7 @@ let discrEq (lbeq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
   Proofview.Goal.enter begin fun gl ->
     let env = Proofview.Goal.env gl in
-    match find_positions env sigma ~no_discr:false t1 t2 with
+    match find_positions env sigma ~keep_proofs:false ~no_discr:false t1 t2 with
     | Inr _ ->
 	tclZEROMSG (str"Not a discriminable equality.")
     | Inl (cpath, (_,dirn), _) ->
@@ -1078,9 +1095,7 @@ let discrEverywhere with_evars =
           (fun id -> tclCOMPLETE (discr with_evars (mkVar id,NoBindings)))))
      else (* <= 8.2 compat *)
        tryAllHypsAndConcl (discrSimpleClause with_evars))
-(*    (fun gls ->
-       user_err ~hdr:"DiscrEverywhere" (str"No discriminable equalities."))
-*)
+
 let discr_tac with_evars = function
   | None -> discrEverywhere with_evars
   | Some c -> onInductionArg (fun clear_flag -> discr with_evars) c
@@ -1402,15 +1417,15 @@ let inject_at_positions env sigma l2r (eq,_,(t,t1,t2)) eq_clause posns tac =
          (if l2r then List.rev injectors else injectors)))
       (tac (List.length injectors)))
 
-let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
+let injEqThen keep_proofs tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
   let sigma = eq_clause.evd in
   let env = eq_clause.env in
-  match find_positions env sigma ~no_discr:true t1 t2 with
+  match find_positions env sigma ~keep_proofs ~no_discr:true t1 t2 with
   | Inl _ ->
      assert false
   | Inr [] ->
      let suggestion =
-         if !keep_proof_equalities_for_injection then
+         if keep_proofs then
             "" else
             " You can try to use option Set Keep Proof Equalities." in
      tclZEROMSG (strbrk("No information can be deduced from this equality and the injectivity of constructors. This may be because the terms are convertible, or due to pattern matching restrictions in the sort Prop." ^ suggestion))
@@ -1429,13 +1444,13 @@ let get_previous_hyp_position id gl =
   in
   aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl))
 
-let injEq ?(old=false) with_evars clear_flag ipats =
+let injEq flags ?(old=false) with_evars clear_flag ipats =
   (* Decide which compatibility mode to use *)
   let ipats_style, l2r, dft_clear_flag, bounded_intro = match ipats with
-    | None when not old && use_injection_in_context () ->
+    | None when not old && use_injection_in_context flags ->
       Some [], true, true, true
     | None -> None, false, false, false
-    | _ -> let b = use_injection_pattern_l2r_order () in ipats, b, b, b in
+    | _ -> let b = use_injection_pattern_l2r_order flags in ipats, b, b, b in
   (* Built the post tactic depending on compatibility mode *)
   let post_tac c n =
     match ipats_style with
@@ -1455,26 +1470,26 @@ let injEq ?(old=false) with_evars clear_flag ipats =
         tclTHEN clear_tac intro_tac
       end
     | None -> tclIDTAC in
-  injEqThen post_tac l2r
+  injEqThen (keep_proof_equalities flags) post_tac l2r
 
-let inj ipats with_evars clear_flag = onEquality with_evars (injEq with_evars clear_flag ipats)
+let inj flags ipats with_evars clear_flag = onEquality with_evars (injEq flags with_evars clear_flag ipats)
 
-let injClause ipats with_evars = function
-  | None -> onNegatedEquality with_evars (injEq with_evars None ipats)
-  | Some c -> onInductionArg (inj ipats with_evars) c
+let injClause flags ipats with_evars = function
+  | None -> onNegatedEquality with_evars (injEq flags with_evars None ipats)
+  | Some c -> onInductionArg (inj flags ipats with_evars) c
 
-let simpleInjClause with_evars = function
-  | None -> onNegatedEquality with_evars (injEq ~old:true with_evars None None)
-  | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq ~old:true with_evars clear_flag None)) c
+let simpleInjClause flags with_evars = function
+  | None -> onNegatedEquality with_evars (injEq flags ~old:true with_evars None None)
+  | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (injEq flags ~old:true with_evars clear_flag None)) c
 
-let injConcl = injClause None false None
-let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.tag id)))
+let injConcl flags = injClause flags None false None
+let injHyp flags clear_flag id = injClause flags None false (Some (clear_flag,ElimOnIdent (Loc.tag id)))
 
-let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
+let decompEqThen keep_proofs ntac (lbeq,_,(t,t1,t2) as u) clause =
   Proofview.Goal.enter begin fun gl ->
     let sigma =  clause.evd in
     let env = Proofview.Goal.env gl in
-      match find_positions env sigma ~no_discr:false t1 t2 with
+      match find_positions env sigma ~keep_proofs ~no_discr:false t1 t2 with
       | Inl (cpath, (_,dirn), _) ->
 	  discr_positions env sigma u clause cpath dirn
       | Inr [] -> (* Change: do not fail, simplify clear this trivial hyp *)
@@ -1484,18 +1499,18 @@ let decompEqThen ntac (lbeq,_,(t,t1,t2) as u) clause =
           (ntac (clenv_value clause))
   end
 
-let dEqThen with_evars ntac = function
-  | None -> onNegatedEquality with_evars (decompEqThen (ntac None))
-  | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (decompEqThen (ntac clear_flag))) c
+let dEqThen ~keep_proofs with_evars ntac = function
+  | None -> onNegatedEquality with_evars (decompEqThen (use_keep_proofs keep_proofs) (ntac None))
+  | Some c -> onInductionArg (fun clear_flag -> onEquality with_evars (decompEqThen (use_keep_proofs keep_proofs) (ntac clear_flag))) c
 
-let dEq with_evars =
-  dEqThen with_evars (fun clear_flag c x ->
+let dEq ~keep_proofs with_evars =
+  dEqThen ~keep_proofs with_evars (fun clear_flag c x ->
     (apply_clear_request clear_flag (use_clear_hyp_by_default ()) c))
 
 let intro_decomp_eq tac data (c, t) =
   Proofview.Goal.enter begin fun gl ->
     let cl = pf_apply make_clenv_binding gl (c, t) NoBindings in
-    decompEqThen (fun _ -> tac) data cl
+    decompEqThen !keep_proof_equalities_for_injection (fun _ -> tac) data cl
   end
 
 let _ = declare_intro_decomp_eq intro_decomp_eq
diff --git a/tactics/equality.mli b/tactics/equality.mli
index a4d1c0f9b..65da2e7dc 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -67,23 +67,31 @@ val replace_in_clause_maybe_by : constr -> constr -> clause -> unit Proofview.ta
 val replace    : constr -> constr -> unit Proofview.tactic
 val replace_by : constr -> constr -> unit Proofview.tactic -> unit Proofview.tactic
 
+type inj_flags = {
+    keep_proof_equalities : bool; (* One may want it or not *)
+    injection_in_context : bool;  (* For regularity; one may want it from ML code but not interactively *)
+    injection_pattern_l2r_order : bool; (* Compatibility option: no reason not to want it *)
+  }
+
 val discr        : evars_flag -> constr with_bindings -> unit Proofview.tactic
 val discrConcl   : unit Proofview.tactic
 val discrHyp     : Id.t -> unit Proofview.tactic
 val discrEverywhere : evars_flag -> unit Proofview.tactic
 val discr_tac    : evars_flag ->
   constr with_bindings destruction_arg option -> unit Proofview.tactic
-val inj          : intro_patterns option -> evars_flag ->
+
+(* Below, if flag is [None], it takes the value from the dynamic value of the option *)
+val inj          : inj_flags option -> intro_patterns option -> evars_flag ->
   clear_flag -> constr with_bindings -> unit Proofview.tactic
-val injClause    : intro_patterns option -> evars_flag ->
+val injClause    : inj_flags option -> intro_patterns option -> evars_flag ->
   constr with_bindings destruction_arg option -> unit Proofview.tactic
-val injHyp       : clear_flag -> Id.t -> unit Proofview.tactic
-val injConcl     : unit Proofview.tactic
-val simpleInjClause : evars_flag ->
+val injHyp       : inj_flags option -> clear_flag -> Id.t -> unit Proofview.tactic
+val injConcl     : inj_flags option -> unit Proofview.tactic
+val simpleInjClause : inj_flags option -> evars_flag ->
   constr with_bindings destruction_arg option -> unit Proofview.tactic
 
-val dEq : evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic
-val dEqThen : evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic
+val dEq : keep_proofs:(bool option) -> evars_flag -> constr with_bindings destruction_arg option -> unit Proofview.tactic
+val dEqThen : keep_proofs:(bool option) -> evars_flag -> (clear_flag -> constr -> int -> unit Proofview.tactic) -> constr with_bindings destruction_arg option -> unit Proofview.tactic
 
 val make_iterated_tuple :
   env -> evar_map -> constr -> (constr * types) -> evar_map * (constr * constr * constr)
@@ -100,7 +108,7 @@ val rewriteInConcl : bool -> constr -> unit Proofview.tactic
 val discriminable : env -> evar_map -> constr -> constr -> bool
 
 (* Tells if tactic "injection" is applicable *)
-val injectable : env -> evar_map -> constr -> constr -> bool
+val injectable : env -> evar_map -> keep_proofs:(bool option) -> constr -> constr -> bool
 
 (* Subst *)
 
diff --git a/tactics/inv.ml b/tactics/inv.ml
index f391382bf..c5aa74ba5 100644
--- a/tactics/inv.ml
+++ b/tactics/inv.ml
@@ -371,7 +371,7 @@ let projectAndApply as_mode thin avoid id eqname names depids =
     (* If no immediate variable in the equation, try to decompose it *)
     (* and apply a trailer which again try to substitute *)
     (fun id ->
-      dEqThen false (deq_trailer id)
+      dEqThen ~keep_proofs:None false (deq_trailer id)
 	(Some (None,ElimOnConstr (EConstr.mkVar id,NoBindings))))
     id