diff options
Diffstat (limited to 'contrib/first-order/ground.ml4')
| -rw-r--r-- | contrib/first-order/ground.ml4 | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/contrib/first-order/ground.ml4 b/contrib/first-order/ground.ml4 index f0cd3afa6..b8f684977 100644 --- a/contrib/first-order/ground.ml4 +++ b/contrib/first-order/ground.ml4 @@ -13,6 +13,7 @@ open Formula open Sequent open Rules +open Instances open Term open Tacmach open Tactics @@ -79,7 +80,8 @@ let ground_tac solver startseq gl= cont_tac gl else (match - Unify.give_right_instances i dom triv atoms seq with + Instances.give_right_instances i dom triv atoms seq + with Some l -> tclORELSE (exists_tac l toptac (re_add seq)) cont_tac gl | None -> |