diff options
Diffstat (limited to 'contrib/romega')
| -rw-r--r-- | contrib/romega/refl_omega.ml | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/contrib/romega/refl_omega.ml b/contrib/romega/refl_omega.ml index 788d3338cf..f87f3db964 100644 --- a/contrib/romega/refl_omega.ml +++ b/contrib/romega/refl_omega.ml @@ -818,6 +818,7 @@ let destructure_hyps gl = loop (pf_ids_of_hyps gl) (pf_hyps gl) gl let omega_solver gl = + Library.check_required_module ["Coq";"romega";"ROmega"]; let concl = pf_concl gl in let rec loop t = match destructurate t with |