From 7741c4884d5823ed745da0c979cfb7322f0902c2 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <Enrico.Tassi@inria.fr>
Date: Wed, 4 Apr 2018 10:52:35 +0200
Subject: ssr: check cleared hyps do exist (fix #7050)

---
 plugins/ssr/ssripats.ml   | 10 +++++++++-
 plugins/ssr/ssrparser.ml4 | 13 +------------
 2 files changed, 10 insertions(+), 13 deletions(-)

(limited to 'plugins/ssr')

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)
-- 
cgit v1.2.3