From 436abd92a520f13843b102b24b61802c88c7dba7 Mon Sep 17 00:00:00 2001 From: Emilio Jesus Gallego Arias Date: Thu, 15 Jun 2017 19:51:06 +0200 Subject: [make] remove compat5 file. It is empty and not used anymore. --- Makefile.common | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'Makefile.common') diff --git a/Makefile.common b/Makefile.common index 85ecb1a08..afd6164fc 100644 --- a/Makefile.common +++ b/Makefile.common @@ -109,7 +109,7 @@ CORECMA:=lib/clib.cma lib/lib.cma kernel/kernel.cma intf/intf.cma library/librar TOPLOOPCMA:=stm/proofworkertop.cma stm/tacworkertop.cma stm/queryworkertop.cma -GRAMMARCMA:=grammar/compat5.cmo grammar/grammar.cma +GRAMMARCMA:=grammar/grammar.cma # modules known by the toplevel of Coq -- cgit v1.2.3