aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--Makefile.build4
-rw-r--r--Makefile.common17
-rw-r--r--toplevel/vernacentries.ml2
3 files changed, 13 insertions, 10 deletions
diff --git a/Makefile.build b/Makefile.build
index e6cba45efb..4fa0438fa1 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -426,8 +426,8 @@ program: $(PROGRAMVO)
structures: $(STRUCTURESVO)
vectors: $(VECTORSVO)
-noreal: logic arith bool zarith qarith lists sets fsets relations \
- wellfounded setoids sorting
+noreal: unicode logic arith bool zarith qarith lists sets fsets \
+ relations wellfounded setoids sorting
###########################################################################
# 3) plugins
diff --git a/Makefile.common b/Makefile.common
index c10a02e265..91498c5dfa 100644
--- a/Makefile.common
+++ b/Makefile.common
@@ -284,13 +284,16 @@ CLASSESVO:=$(call cat_vo_itarget, theories/Classes)
PROGRAMVO:=$(call cat_vo_itarget, theories/Program)
THEORIESVO:=\
- $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) $(PARITHVO) $(NARITHVO) $(ZARITHVO) \
- $(SETOIDSVO) $(LISTSVO) $(STRINGSVO) $(SETSVO) $(FSETSVO) $(MSETSVO) \
- $(RELATIONSVO) $(WELLFOUNDEDVO) $(REALSVO) $(SORTINGVO) $(QARITHVO) \
- $(NUMBERSVO) $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) $(STRUCTURESVO) \
- $(VECTORSVO)
-
-THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(ARITHVO)
+ $(INITVO) $(LOGICVO) $(ARITHVO) $(BOOLVO) \
+ $(UNICODEVO) $(CLASSESVO) $(PROGRAMVO) \
+ $(RELATIONSVO) $(WELLFOUNDEDVO) $(SETOIDSVO) \
+ $(LISTSVO) $(STRINGSVO) \
+ $(PARITHVO) $(NARITHVO) $(ZARITHVO) \
+ $(SETSVO) $(FSETSVO) $(MSETSVO) \
+ $(REALSVO) $(SORTINGVO) $(QARITHVO) \
+ $(NUMBERSVO) $(STRUCTURESVO) $(VECTORSVO)
+
+THEORIESLIGHTVO:= $(INITVO) $(LOGICVO) $(UNICODEVO) $(ARITHVO)
## Plugins
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 5c8efd3f89..2235dd8806 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -586,7 +586,7 @@ let vernac_scheme l =
let vernac_combined_scheme lid l =
if Dumpglob.dump () then
(Dumpglob.dump_definition lid false "def";
- List.iter (fun lid -> dump_global (AN (Ident lid))) l);
+ List.iter (fun lid -> dump_global (Misctypes.AN (Ident lid))) l);
Indschemes.do_combined_scheme lid l
(**********************)