From 295107103aaa86db8a31abb0e410123212648d45 Mon Sep 17 00:00:00 2001
From: Pierre Letouzey <pierre.letouzey@inria.fr>
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.
---
 Makefile.common | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

(limited to 'Makefile.common')

diff --git a/Makefile.common b/Makefile.common
index b2e1d47df..ec5e6ac85 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -129,8 +129,8 @@ RTAUTOCMO:=plugins/rtauto/rtauto_plugin.cmo
 NATSYNTAXCMO:=plugins/syntax/nat_syntax_plugin.cmo
 OTHERSYNTAXCMO:=$(addprefix plugins/syntax/, \
         z_syntax_plugin.cmo \
-        numbers_syntax_plugin.cmo \
         r_syntax_plugin.cmo \
+	int31_syntax_plugin.cmo \
 	ascii_syntax_plugin.cmo \
         string_syntax_plugin.cmo )
 DERIVECMO:=plugins/derive/derive_plugin.cmo
@@ -161,14 +161,8 @@ LINKCMX:=$(CORECMA:.cma=.cmxa) $(STATICPLUGINS:.cmo=.cmx)
 # vo files
 ###########################################################################
 
-GENVOFILES := $(GENVFILES:.v=.vo)
-
-THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v")) \
-              $(filter theories/%, $(GENVOFILES))
-
-PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v")) \
-             $(filter plugins/%, $(GENVOFILES))
-
+THEORIESVO := $(patsubst %.v,%.vo,$(shell find theories -type f -name "*.v"))
+PLUGINSVO := $(patsubst %.v,%.vo,$(shell find plugins -type f -name "*.v"))
 ALLVO := $(THEORIESVO) $(PLUGINSVO)
 VFILES := $(ALLVO:.vo=.v)
 
-- 
cgit v1.2.3