From f61a557fbbdb89a4c24a8050a67252c3ecda6ea7 Mon Sep 17 00:00:00 2001 From: letouzey Date: Thu, 5 May 2011 15:12:09 +0000 Subject: Definitions of positive, N, Z moved in Numbers/BinNums.v In the coming reorganisation, the name Z in BinInt will be a module containing all code and properties about binary integers. The inductive type Z hence cannot be at the same location. Same for N and positive. Apart for this naming constraint, it also have advantages : presenting the three types at once is clearer, and we will be able to refer to N in BinPos (for instance for output type of a predecessor function on positive). git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14097 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/rtauto/refl_tauto.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/rtauto') 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") -- cgit v1.2.3