[wp] split conjunctions only when looking in hyps

src/plugins/wp/Pattern.ml

@@ -449,10 +449,11 @@ type lookup = {
   head: bool ;
   goal: bool ;
   hyps: bool ;
+  split: bool ;
   pattern: pattern ;
 }
 
-let pclause { head ; pattern } clause sigma prop =
+let pclause { head ; pattern ; split } clause sigma prop =
   let tprop = Lang.F.e_prop prop in
   let select t =
     if t == tprop then Tactical.Clause clause else Tactical.Inside(clause,t) in
@@ -462,7 +463,7 @@ let pclause { head ; pattern } clause sigma prop =
     then Some env.sigma else None
   in
   match Lang.F.repr tprop with
-  | And ts -> plist pcond ts
+  | And ts when split -> plist pcond ts
   | _ -> pcond tprop
 
 (* --- Step Ordering --- *)

src/plugins/wp/Pattern.mli

@@ -54,6 +54,7 @@ type lookup = {
   head: bool ;
   goal: bool ;
   hyps: bool ;
+  split: bool ;
   pattern: pattern ;
 }
 

src/plugins/wp/ProofStrategy.ml

@@ -176,8 +176,9 @@ let parse_name ctxt ~kind ?check p =
     { loc ; value }
   | _ -> ctxt.error loc "%s name expected (%a)" kind debug p
 
-let parse_lookup penv ?(head=true) ?(goal=false) ?(hyps=false) p =
-  { goal ; hyps ; head ; pattern = Pattern.pa_pattern penv p }
+let parse_lookup penv
+    ?(head=true) ?(goal=false) ?(hyps=false) ?(split=false) p =
+  { goal ; hyps ; head ; split ; pattern = Pattern.pa_pattern penv p }
 
 let autoselect select lookup =
   match select , lookup with
@@ -208,7 +209,7 @@ let rec parse_tactic_params ctxt penv
       let lookup = List.rev_append qs lookup in
       cc ~select ~lookup ~params ~children ~default ps
     | PLapp("\\when",[],qs) ->
-      let qs = List.map (parse_lookup ~hyps:true penv) qs in
+      let qs = List.map (parse_lookup ~hyps:true ~split:true penv) qs in
       let lookup = List.rev_append qs lookup in
       cc ~select ~lookup ~params ~children ~default ps
     | PLapp("\\ingoal",[],qs) ->
@@ -216,7 +217,7 @@ let rec parse_tactic_params ctxt penv
       let lookup = List.rev_append qs lookup in
       cc ~select ~lookup ~params ~children ~default ps
     | PLapp("\\incontext",[],qs) ->
-      let qs = List.map (parse_lookup ~head:false ~hyps:true penv) qs in
+      let qs = List.map (parse_lookup ~head:false ~hyps:true ~split:true penv) qs in
       let lookup = List.rev_append qs lookup in
       cc ~select ~lookup ~params ~children ~default ps
     | PLapp("\\pattern",[],qs) ->