From 80e21990d36224f2b06bf131cbc87dbfbd274af0 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
Date: Wed, 10 May 2017 17:35:13 +0200
Subject: romega: if it bugs again, at least do it with a short and quick error

---
 plugins/romega/ReflOmegaCore.v | 14 +++++++++-----
 1 file changed, 9 insertions(+), 5 deletions(-)

(limited to 'plugins/romega')

diff --git a/plugins/romega/ReflOmegaCore.v b/plugins/romega/ReflOmegaCore.v
index 1d24c8c21..2c8879e66 100644
--- a/plugins/romega/ReflOmegaCore.v
+++ b/plugins/romega/ReflOmegaCore.v
@@ -2879,6 +2879,10 @@ Proof.
  red. intros. now apply H.
 Qed.
 
+(** Attempt to shorten error messages if romega goes rogue...
+    NB: [interp_list_goal _ _ BUG = False /\ True]. *)
+Definition BUG : lhyps := nil :: nil.
+
 Fixpoint decompose_solve (s : e_step) (h : hyps) {struct s} : lhyps :=
   match s with
   | E_SPLIT i dl s1 s2 =>
@@ -2889,12 +2893,12 @@ Fixpoint decompose_solve (s : e_step) (h : hyps) {struct s} : lhyps :=
           then
            decompose_solve s1 (Tnot x :: h) ++
            decompose_solve s2 (Tnot y :: h)
-          else h :: nil
+          else BUG
       | Timp x y =>
           if decidability x then
             decompose_solve s1 (Tnot x :: h) ++ decompose_solve s2 (y :: h)
-          else h::nil
-      | _ => h :: nil
+          else BUG
+      | _ => BUG
       end
   | E_EXTRACT i dl s1 =>
       decompose_solve s1 (extract_hyp_pos dl (nth_hyps i h) :: h)
@@ -2939,9 +2943,9 @@ Definition valid_lhyps (f : lhyps -> lhyps) :=
 
 Fixpoint reduce_lhyps (lp : lhyps) : lhyps :=
   match lp with
+  | nil => nil
   | (FalseTerm :: nil) :: lp' => reduce_lhyps lp'
-  | x :: lp' => x :: reduce_lhyps lp'
-  | nil => nil (A:=hyps)
+  | x :: lp' => BUG
   end.
 
 Theorem reduce_lhyps_valid : valid_lhyps reduce_lhyps.
-- 
cgit v1.2.3