From b4bdf9f6e7085ce2ba4e9eaaaa6c594bd473cd07 Mon Sep 17 00:00:00 2001
From: ineol <leo.lveb@gmail.com>
Date: Thu, 3 Oct 2024 23:37:56 +0200
Subject: [PATCH] Make `bv_automata` fallible (#670)

Currently, `bv_automata` does not fail if the goal is false, because
`native_decide` doesn't fail, it produces an ill-typed proof.

On consequence is that it is awkward to use `bv_automata` in a tactic
such as `bv_auto`, since it relied on tactics to fail to be able to try
the next tactic (cf issue #660) It also give an error that is not
helpful at all after the proof is complete.

This PR is a proof of concept that modifies the implementation of
`native_decide` to check that the problem is solved by the decision
procedure before constructing the proof object.