[pose]: do not use conversion when matching did not use it

Author: strub

src/ecHiGoal.ml

@@ -729,23 +729,26 @@ let process_delta ~und_delta ?target (s, o, p) tc =
         with EcEnv.NotReducible -> fp
     in
 
-    let matches =
-      try  ignore (PT.pf_find_occurence ptenv ~ptn:fp target); true
-      with PT.FindOccFailure _ -> false
-    in
+    begin
+      match PT.pf_find_occurence ptenv ~ptn:fp target with
+      | (_, occmode) ->
+        let p    = concretize_form ptenv p  in
+        let fp   = concretize_form ptenv fp in
+        let cpos =
+          try
+            FPosition.select_form
+              ~xconv:(if occmode.k_conv then `Conv else `AlphaEq)
+              ~keyed:occmode.k_keyed
+              hyps o fp target
+          with InvalidOccurence ->
+            tc_error !!tc "invalid occurences selector" in
 
-    if matches then begin
-      let p    = concretize_form ptenv p  in
-      let fp   = concretize_form ptenv fp in
-      let cpos =
-        try  FPosition.select_form hyps o fp target
-        with InvalidOccurence ->
-          tc_error !!tc "invalid occurences selector"
-      in
+        let target = FPosition.map cpos (fun _ -> p) target in
+        t_change ~ri ?target:idtg target tc 
 
-      let target = FPosition.map cpos (fun _ -> p) target in
-      t_change ~ri ?target:idtg target tc
-    end else t_id tc
+      | exception (PT.FindOccFailure _) ->
+        t_id tc
+  end
 
 (* -------------------------------------------------------------------- *)
 let process_rewrite1_r ttenv ?target ri tc =