From 1b3c25792c0598ae0cc44e9db1e7bde3f5789638 Mon Sep 17 00:00:00 2001 From: Hugo Herbelin Date: Sat, 31 Mar 2018 15:03:27 +0200 Subject: Splitting primitive numeral parser/printer for positive, N, Z into three files. --- theories/Numbers/BinNums.v | 2 ++ 1 file changed, 2 insertions(+) (limited to 'theories') diff --git a/theories/Numbers/BinNums.v b/theories/Numbers/BinNums.v index f8b3d9e1d..d5eb4f268 100644 --- a/theories/Numbers/BinNums.v +++ b/theories/Numbers/BinNums.v @@ -12,6 +12,8 @@ Set Implicit Arguments. +Declare ML Module "positive_syntax_plugin". +Declare ML Module "n_syntax_plugin". Declare ML Module "z_syntax_plugin". (** [positive] is a datatype representing the strictly positive integers -- cgit v1.2.3