diff options
| author |  Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-10 17:35:13 +0200 |
|---|---|---|
| committer | Pierre Letouzey <pierre.letouzey@inria.fr> | 2017-05-22 15:15:49 +0200 |
| commit | 80e21990d36224f2b06bf131cbc87dbfbd274af0 (patch) | |
| tree | bce2fe4307c643d484cc508011b4cf5717aa5a37 | |
| parent | 7ffb02d2c5534a6c39ee1e5fd42060d559195e39 (diff) | |
romega: if it bugs again, at least do it with a short and quick error
| -rw-r--r-- | plugins/romega/ReflOmegaCore.v | 14 |
1 files changed, 9 insertions, 5 deletions
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. |