diff options
Diffstat (limited to 'plugins/rtauto/refl_tauto.ml')
| -rw-r--r-- | plugins/rtauto/refl_tauto.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/rtauto/refl_tauto.ml b/plugins/rtauto/refl_tauto.ml index a520ce2d4..cddc5472d 100644 --- a/plugins/rtauto/refl_tauto.ml +++ b/plugins/rtauto/refl_tauto.ml @@ -36,7 +36,7 @@ let l_true_equals_true = [|data_constant "bool";data_constant "true"|])) let pos_constant = - Coqlib.gen_constant "refl_tauto" ["PArith";"BinPos"] + Coqlib.gen_constant "refl_tauto" ["Numbers";"BinNums"] let l_xI = lazy (pos_constant "xI") let l_xO = lazy (pos_constant "xO") |