Giving a more natural semantics to injection by default.

There were three versions of injection:

1. "injection term" without "as" clause:
   was leaving hypotheses on the goal in reverse order
2. "injection term as ipat", first version:
   was introduction hypotheses using ipat in reverse order without
   checking that the number of ipat was the size of the injection
   (activated with "Unset Injection L2R Pattern Order")
3. "injection term as ipat", second version:
   was introduction hypotheses using ipat in left-to-right order
   checking that the number of ipat was the size of the injection
   and clearing the injecting term by default if an hypothesis
   (activated with "Set Injection L2R Pattern Order", default one from 8.5)

There is now:

4. "injection term" without "as" clause, new version:
   introducing the components of the injection in the context in
   left-to-right order using default intro-patterns "?"
   and clearing the injecting term by default if an hypothesis
   (activated with "Set Structural Injection")

The new versions 3. and 4. are the "expected" ones in the sense that
they have the following good properties:
- introduction in the context is in the natural left-to-right order
- "injection" behaves the same with and without "as", always
  introducing the hypotheses in the goal what corresponds to the
  natural expectation as the changes I made in the proof scripts for
  adaptation confirm
- clear the "injection" hypothesis when an hypothesis which is the
  natural expectation as the changes I made in the proof scripts for
  adaptation confirm

The compatibility can be preserved by "Unset Structural Injection" or
by calling "simple injection".

The flag is currently off.

2 files changed, 56 insertions, 21 deletions

diff --git a/tactics/equality.ml b/tactics/equality.ml
index db7d2e4a13..1d3239ef68 100644
--- a/tactics/equality.ml
+++ b/tactics/equality.ml
@@ -72,11 +72,26 @@ let _ =
   declare_bool_option
     { optsync  = true;
       optdepr  = false;
-      optname  = "injection left-to-right pattern order";
+      optname  = "injection left-to-right pattern order and clear by default when with introduction pattern";
       optkey   = ["Injection";"L2R";"Pattern";"Order"];
       optread  = (fun () -> !injection_pattern_l2r_order) ;
       optwrite = (fun b -> injection_pattern_l2r_order := b) }
 
+let injection_in_context = ref false
+
+let use_injection_in_context () =
+  !injection_in_context
+  && Flags.version_strictly_greater Flags.V8_5
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "injection in context";
+      optkey   = ["Structural";"Injection"];
+      optread  = (fun () -> !injection_in_context) ;
+      optwrite = (fun b -> injection_in_context := b) }
+
 (* Rewriting tactics *)
 
 let tclNOTSAMEGOAL tac =
@@ -1381,27 +1396,41 @@ let injEqThen tac l2r (eq,_,(t,t1,t2) as u) eq_clause =
       inject_at_positions env sigma l2r u eq_clause posns
 	(tac (clenv_value eq_clause))
 
-let use_clear_hyp_by_default () = false
-
-let postInjEqTac with_evars clear_flag ipats c n =
-  match ipats with
-  | Some ipats ->
-      let clear_tac =
-        let dft =
-          use_injection_pattern_l2r_order () || use_clear_hyp_by_default () in
-        tclTRY (apply_clear_request clear_flag dft c) in
-      let intro_tac =
-        if use_injection_pattern_l2r_order ()
-        then intro_patterns_bound_to with_evars n MoveLast ipats
-        else intro_patterns_to with_evars MoveLast ipats in
-      tclTHEN clear_tac intro_tac
-  | None -> apply_clear_request clear_flag false c
-
-let injEq with_evars clear_flag ipats =
-  let l2r =
-    if use_injection_pattern_l2r_order () && not (Option.is_empty ipats) then true else false
+let get_previous_hyp_position id gl =
+  let rec aux dest = function
+  | [] -> raise (RefinerError (NoSuchHyp id))
+  | d :: right ->
+    let hyp = Context.Named.Declaration.get_id d in
+    if Id.equal hyp id then dest else aux (MoveAfter hyp) right
   in
-  injEqThen (fun c i -> postInjEqTac with_evars clear_flag ipats c i) l2r
+  aux MoveLast (Proofview.Goal.hyps (Proofview.Goal.assume gl))
+
+let injEq ?(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 () ->
+      Some [], true, true, true
+    | None -> None, false, false, false
+    | _ -> let b = use_injection_pattern_l2r_order () in ipats, b, b, b in
+  (* Built the post tactic depending on compatibility mode *)
+  let post_tac c n =
+    match ipats_style with
+    | Some ipats ->
+      Proofview.Goal.enter { enter = begin fun gl ->
+        let destopt = match kind_of_term c with
+        | Var id -> get_previous_hyp_position id gl
+        | _ -> MoveLast in
+        let clear_tac =
+          tclTRY (apply_clear_request clear_flag dft_clear_flag c) in
+        (* Try should be removal if dependency were treated *)
+        let intro_tac =
+          if bounded_intro
+          then intro_patterns_bound_to with_evars n destopt ipats
+          else intro_patterns_to with_evars destopt ipats in
+        tclTHEN clear_tac intro_tac
+      end }
+    | None -> tclIDTAC in
+  injEqThen post_tac l2r
 
 let inj ipats with_evars clear_flag = onEquality with_evars (injEq with_evars clear_flag ipats)
 
@@ -1409,6 +1438,10 @@ let injClause ipats with_evars = function
   | None -> onNegatedEquality with_evars (injEq with_evars None ipats)
   | Some c -> onInductionArg (inj 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 injConcl = injClause None false None
 let injHyp clear_flag id = injClause None false (Some (clear_flag,ElimOnIdent (Loc.ghost,id)))
 
diff --git a/tactics/equality.mli b/tactics/equality.mli
index 1122615c3d..47cb6b82fd 100644
--- a/tactics/equality.mli
+++ b/tactics/equality.mli
@@ -79,6 +79,8 @@ val injClause    : 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 ->
+  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