ssr: check cleared hyps do exist (fix #7050)

4 files changed, 19 insertions, 13 deletions

diff --git a/plugins/ssr/ssripats.ml b/plugins/ssr/ssripats.ml
index 42566575c..7897cb170 100644
--- a/plugins/ssr/ssripats.ml
+++ b/plugins/ssr/ssripats.ml
@@ -133,6 +133,12 @@ let intro_clear ids future_ipats =
     isCLR_PUSHL clear_ids
 end
 
+let tacCHECK_HYPS_EXIST hyps = Goal.enter begin fun gl ->
+  let ctx = Goal.hyps gl in
+  List.iter (Ssrcommon.check_hyp_exists ctx) hyps;
+  tclUNIT ()
+end
+
 (** [=> []] *****************************************************************)
 let tac_case t =
   Goal.enter begin fun _ ->
@@ -229,7 +235,9 @@ let rec ipat_tac1 future_ipats ipat : unit tactic =
   | IPatNoop -> tclUNIT ()
   | IPatSimpl Nop -> tclUNIT ()
 
-  | IPatClear ids -> intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats
+  | IPatClear ids ->
+      tacCHECK_HYPS_EXIST ids <*>
+      intro_clear (List.map Ssrcommon.hyp_id ids) future_ipats
 
   | IPatSimpl (Simpl n) ->
        V82.tactic ~nf_evars:false (Ssrequality.simpltac (Simpl n))
diff --git a/plugins/ssr/ssrparser.ml4 b/plugins/ssr/ssrparser.ml4
index 0d82a9f09..5f3967440 100644
--- a/plugins/ssr/ssrparser.ml4
+++ b/plugins/ssr/ssrparser.ml4
@@ -585,21 +585,10 @@ let pr_ssripat _ _ _ = pr_ipat
 let pr_ssripats _ _ _ = pr_ipats
 let pr_ssriorpat _ _ _ = pr_iorpat
 
-(*
-let intern_ipat ist ipat =
-  let rec check_pat = function
-  | IPatClear clr -> ignore (List.map (intern_hyp ist) clr)
-  | IPatCase iorpat -> List.iter (List.iter check_pat) iorpat
-  | IPatDispatch iorpat -> List.iter (List.iter check_pat) iorpat
-  | IPatInj iorpat -> List.iter (List.iter check_pat) iorpat
-  | _ -> () in
-  check_pat ipat; ipat
-*)
-
 let intern_ipat ist =
   map_ipat
     (fun id -> id)
-    (intern_hyp ist) (* TODO: check with ltac, old code was ignoring the result *)
+    (intern_hyp ist)
     (glob_ast_closure_term ist)
 
 let intern_ipats ist = List.map (intern_ipat ist)
diff --git a/test-suite/output/ssr_clear.out b/test-suite/output/ssr_clear.out
new file mode 100644
index 000000000..151595406
--- /dev/null
+++ b/test-suite/output/ssr_clear.out
@@ -0,0 +1,3 @@
+The command has indeed failed with message:
+Ltac call to "move (ssrmovearg) (ssrclauses)" failed.
+No assumption is named NO_SUCH_NAME
diff --git a/test-suite/output/ssr_clear.v b/test-suite/output/ssr_clear.v
new file mode 100644
index 000000000..573ec47e0
--- /dev/null
+++ b/test-suite/output/ssr_clear.v
@@ -0,0 +1,6 @@
+Require Import ssreflect.
+
+Example foo : True -> True.
+Proof.
+Fail move=> {NO_SUCH_NAME}.
+Abort.