From 295107103aaa86db8a31abb0e410123212648d45 Mon Sep 17 00:00:00 2001 From: Pierre Letouzey Date: Wed, 22 Mar 2017 11:24:27 +0100 Subject: BigNums: remove files about BigN,BigZ,BigQ (now in an separate git repo) See now https://github.com/coq/bignums Int31 is still in the stdlib. Some proofs there has be adapted to avoid the need for BigNumPrelude. --- plugins/syntax/int31_syntax_plugin.mlpack | 1 + 1 file changed, 1 insertion(+) create mode 100644 plugins/syntax/int31_syntax_plugin.mlpack (limited to 'plugins/syntax/int31_syntax_plugin.mlpack') diff --git a/plugins/syntax/int31_syntax_plugin.mlpack b/plugins/syntax/int31_syntax_plugin.mlpack new file mode 100644 index 000000000..54a5bc0cd --- /dev/null +++ b/plugins/syntax/int31_syntax_plugin.mlpack @@ -0,0 +1 @@ +Int31_syntax -- cgit v1.2.3