From 25893b01cb815cbd9a3b9684952bfc0f42c0739d Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 29 Dec 2015 15:11:23 +0000 Subject: [PATCH] - final commit for helena 0.8.3 minir bugs fixed --- helm/software/helena/Make | 5 +- helm/software/helena/MakeVersion | 2 +- helm/software/helena/Makefile | 84 ++++++++++--------- helm/software/helena/Makefile.common | 2 +- helm/software/helena/README | 36 ++++++-- .../{ => scripts}/coq/grundlagen.template | 0 .../helena/{ => scripts}/coq/grundlagen_2.v | 2 +- .../{ => scripts}/coq/grundlagen_2_ver.v | 0 .../helena/{ => scripts}/lp/lp.template | 0 .../{ => scripts}/matita/grundlagen_2.ma | 2 +- .../{ => scripts}/matita/grundlagen_2_0.ma | 0 .../{ => scripts}/matita/grundlagen_2_1.ma | 0 .../{ => scripts}/matita/grundlagen_2_2.ma | 0 .../{ => scripts}/matita/grundlagen_2_3.ma | 0 .../{ => scripts}/matita/grundlagen_2_4.ma | 0 .../{ => scripts}/matita/grundlagen_2_5.ma | 0 .../{ => scripts}/matita/grundlagen_2_6.ma | 0 .../software/helena/{ => scripts}/matita/root | 0 .../software/helena/src/automath/autLexer.mll | 15 ++-- .../helena/src/basic_rg/brgReduction.ml | 11 +-- helm/software/helena/src/common/options.ml | 6 +- 21 files changed, 95 insertions(+), 70 deletions(-) rename helm/software/helena/{ => scripts}/coq/grundlagen.template (100%) rename helm/software/helena/{ => scripts}/coq/grundlagen_2.v (99%) rename helm/software/helena/{ => scripts}/coq/grundlagen_2_ver.v (100%) rename helm/software/helena/{ => scripts}/lp/lp.template (100%) rename helm/software/helena/{ => scripts}/matita/grundlagen_2.ma (99%) rename helm/software/helena/{ => scripts}/matita/grundlagen_2_0.ma (100%) rename helm/software/helena/{ => scripts}/matita/grundlagen_2_1.ma (100%) rename helm/software/helena/{ => scripts}/matita/grundlagen_2_2.ma (100%) rename helm/software/helena/{ => scripts}/matita/grundlagen_2_3.ma (100%) rename helm/software/helena/{ => scripts}/matita/grundlagen_2_4.ma (100%) rename helm/software/helena/{ => scripts}/matita/grundlagen_2_5.ma (100%) rename helm/software/helena/{ => scripts}/matita/grundlagen_2_6.ma (100%) rename helm/software/helena/{ => scripts}/matita/root (100%) diff --git a/helm/software/helena/Make b/helm/software/helena/Make index 157c04483..058236bd8 100644 --- a/helm/software/helena/Make +++ b/helm/software/helena/Make @@ -3,8 +3,9 @@ Make* README examples/automath/*.aut examples/automath/README -coq/*.v -coq/*.template +scripts/coq/*.v +scripts/coq/*.template +scripts/lp/*.template src/*.ml src/Make* src/*/* diff --git a/helm/software/helena/MakeVersion b/helm/software/helena/MakeVersion index 100435be1..ee94dd834 100644 --- a/helm/software/helena/MakeVersion +++ b/helm/software/helena/MakeVersion @@ -1 +1 @@ -0.8.2 +0.8.3 diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile index 48f7e4b96..6194e6c4c 100644 --- a/helm/software/helena/Makefile +++ b/helm/software/helena/Makefile @@ -33,16 +33,18 @@ INPUT = examples/automath/grundlagen_2.aut INPUTFAST = examples/automath/grundlagen_1.aut +OUTPUT = scripts + MA = grundlagen_2.ma V = grundlagen_2.v LP1 = grundlagen_21.elpi LP2 = grundlagen_22.elpi TJ2 = grundlagen_22.mod -TJ2 = grundlagen_23.mod +TJ3 = grundlagen_23.mod PREAMBLE_MA = ../matita/matita.ma.templ -PREAMBLE_V = coq/grundlagen.template -PREAMBLE_LP = lp/lp.template +PREAMBLE_V = $(OUTPUT)/coq/grundlagen.template +PREAMBLE_LP = $(OUTPUT)/lp/lp.template ALL_FEATURES = LEXER PARSER TRACE SUMMARY EXPAND MANAGER OBJECTS PREPROCESS QUOTE STAGE TYPE @@ -61,8 +63,8 @@ byte: .depend.byte @$(CALLMAKE) F="$(ALL_FEATURES)" $(MAIN).byte test-si-fast: $(MAIN).opt etc - @echo " HELENA -q -u -x -y -1 $(INPUTFAST)" - $(H)./$(MAIN).opt -T 1 -q -u -x -y -1 $(O) $(INPUTFAST) > etc/log.txt + @echo " HELENA -u -x -y -1 $(INPUTFAST)" + $(H)./$(MAIN).opt -T 1 -u -x -y -1 $(O) $(INPUTFAST) > etc/log.txt test-si: $(MAIN).opt etc @echo " HELENA -d -l -u -0 $(INPUT)" @@ -89,25 +91,25 @@ test6: $(MAIN).opt etc $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -T 6 -l $(O) $(INPUT) > etc/log.txt profile-fast: $(MAIN).opt etc - @echo " HELENA -q -u -x $(INPUTFAST) (31 TIMES)" + @echo " HELENA -u -x -y -1 $(INPUTFAST) (31 TIMES)" $(H)rm -f etc/log.txt - $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -q -u -x -1 $(O) $(INPUTFAST) >> etc/log.txt; done + $(H)for T in `seq 31`; do ./$(MAIN).opt -T 1 -u -x -y -1 $(O) $(INPUTFAST) >> etc/log.txt; done $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt profile: $(MAIN).opt etc - @echo " HELENA -l -u $(INPUT) (31 TIMES)" + @echo " HELENA -l -u -1 $(INPUT) (31 TIMES)" $(H)rm -f etc/log.txt $(H)for _ in `seq 31`; do ./$(MAIN).opt $(TEST1) >> etc/log.txt; done $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile.txt profile-opt: $(MAIN).opt etc - @echo " HELENA -l $(INPUT) (31 TIMES)" + @echo " HELENA -l -1 $(INPUT) (31 TIMES)" $(H)rm -f etc/log.txt $(H)for _ in `seq 31`; do ./$(MAIN).opt $(TEST1) $(TEST2) >> etc/log.txt; done $(H)grep "processed" etc/log.txt | sort -k 6 | uniq > etc/profile.txt profile-byte: $(MAIN).byte etc - @echo " HELENA -l $(INPUT) (31 TIMES)" + @echo " HELENA -l -1 $(INPUT) (31 TIMES)" $(H)rm -f etc/log.txt $(H)for _ in `seq 31`; do ./$(MAIN).byte $(TEST1) $(TEST2) >> etc/log.txt; done $(H)grep "processed" etc/log.txt | sort -k 6 | uniq > etc/profile.txt @@ -115,67 +117,67 @@ profile-byte: $(MAIN).byte etc profile-coq: $(MAIN).opt etc @echo " COQTOP $(V) (31 TIMES)" $(H)rm -f etc/log.txt - $(H)for _ in `seq 31`; do echo Load \"coq/$(V)\". | $(TIME) $(COQTOP) -q $(NULL); done + $(H)for _ in `seq 31`; do echo Load \"$(OUTPUT)/coq/$(V)\". | $(TIME) $(COQTOP) -q $(NULL); done $(H)grep -h user etc/log.txt | sort | uniq > etc/profile.txt profile-coq-byte: $(MAIN).opt etc @echo " COQTOP $(V) (31 TIMES)" $(H)rm -f etc/log.txt - $(H)for _ in `seq 31`; do echo Load \"coq/$(V)\". | $(TIME) $(COQTOP).byte -q $(NULL); done + $(H)for _ in `seq 31`; do echo Load \"$(OUTPUT)/coq/$(V)\". | $(TIME) $(COQTOP).byte -q $(NULL); done $(H)grep -h user etc/log.txt | sort | uniq > etc/profile.txt xml-si: $(MAIN).opt etc - @echo " HELENA -l -o -s 1 -u -y $(INPUT)" - $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 1 -u -y $(O) $(INPUT) > etc/log.txt + @echo " HELENA -l -o -q -s 1 -u -y $(INPUT)" + $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -q -s 1 -u -y $(O) $(INPUT) > etc/log.txt xml-si-v3: $(MAIN).opt etc - @echo " HELENA -l -o -s 2 -u -y $(INPUT)" - $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -s 2 -u -y $(O) $(INPUT) > etc/log.txt + @echo " HELENA -l -o -q -s 2 -u -y $(INPUT)" + $(H)./$(MAIN).opt -O $(XMLDIR) -T 1 -l -o -q -s 2 -u -y $(O) $(INPUT) > etc/log.txt xml: $(MAIN).opt etc - @echo " HELENA -l -o -s 1 -y $(INPUT)" - $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 1 -y $(O) $(INPUT) > etc/log.txt + @echo " HELENA -l -o -q -s 1 -y $(INPUT)" + $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -q -s 1 -y $(O) $(INPUT) > etc/log.txt xml-v3: $(MAIN).opt etc - @echo " HELENA -l -o -s 2 $(INPUT)" - $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -s 2 -y $(O) $(INPUT) > etc/log.txt + @echo " HELENA -l -o -q -s 2 -y $(INPUT)" + $(H)./$(MAIN).opt -l -u $(O) $(INPUT) -X -O $(XMLDIR) -T 1 -l -o -q -s 2 -y $(O) $(INPUT) > etc/log.txt -export-coq coq/$(V): $(MAIN).opt etc - @echo " HELENA -m V8 $(INPUT)" - $(H)./$(MAIN).opt -a n -m V8 -p $(PREAMBLE_V) $(TEST1) > etc/log.txt +export-coq $(OUTPUT)/coq/$(V): $(MAIN).opt etc + @echo " HELENA -m V8 -q $(INPUT)" + $(H)./$(MAIN).opt -M $(OUTPUT) -a n -m V8 -p $(PREAMBLE_V) -q $(TEST1) > etc/log.txt -export-matita matita/$(MA): $(MAIN).opt etc - @echo " HELENA -m MA2 $(INPUT)" - $(H)./$(MAIN).opt -a n -m MA2 -p $(PREAMBLE_MA) $(TEST1) > etc/log.txt +export-matita $(OUTPUT)/matita/$(MA): $(MAIN).opt etc + @echo " HELENA -m MA2 -q $(INPUT)" + $(H)./$(MAIN).opt -M $(OUTPUT) -a n -m MA2 -p $(PREAMBLE_MA) -q $(TEST1) > etc/log.txt -export-lp1 lp/$(LP1): $(MAIN).opt etc - @echo " HELENA -m LP1 $(INPUT)" - $(H)./$(MAIN).opt -a n -m LP1 -p $(PREAMBLE_LP) $(TEST1) > etc/log.txt +export-lp1 $(OUTPUT)/lp/$(LP1): $(MAIN).opt etc + @echo " HELENA -m LP1 -q $(INPUT)" + $(H)./$(MAIN).opt -M $(OUTPUT) -a n -m LP1 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt -export-lp2 lp/$(LP2): $(MAIN).opt etc - @echo " HELENA -m LP2 $(INPUT)" - $(H)./$(MAIN).opt -a n -m LP2 -p $(PREAMBLE_LP) $(TEST1) > etc/log.txt +export-lp2 $(OUTPUT)/lp/$(LP2): $(MAIN).opt etc + @echo " HELENA -m LP2 -q $(INPUT)" + $(H)./$(MAIN).opt -M $(OUTPUT) -a n -m LP2 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt -export-tj2 lp/$(TJ2): $(MAIN).opt etc - @echo " HELENA -m TJ2 $(INPUT)" - $(H)./$(MAIN).opt -a n -m TJ2 -p $(PREAMBLE_LP) $(TEST1) > etc/log.txt +export-tj2 $(OUTPUT)/lp/$(TJ2): $(MAIN).opt etc + @echo " HELENA -m TJ2 -q $(INPUT)" + $(H)./$(MAIN).opt -M $(OUTPUT) -a n -m TJ2 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt -export-tj3 lp/$(TJ3): $(MAIN).opt etc - @echo " HELENA -m TJ3 $(INPUT)" - $(H)./$(MAIN).opt -a n -m TJ3 -p $(PREAMBLE_LP) $(TEST1) > etc/log.txt +export-tj3 $(OUTPUT)/lp/$(TJ3): $(MAIN).opt etc + @echo " HELENA -m TJ3 -q $(INPUT)" + $(H)./$(MAIN).opt -M $(OUTPUT) -a n -m TJ3 -p $(PREAMBLE_LP) -q $(TEST1) > etc/log.txt -matita: matita/$(MA) +matita: $(OUTPUT)/matita/$(MA) @echo " MATITA $(MA)" $(H)cd matita && $(MATITA) $(MA) -matitac: matita/$(MA) +matitac: $(OUTPUT)/matita/$(MA) @echo " MATITAC $(MA)" $(H)cd matita && $(MATITAC) $(MA) #profile-matita: $(MAIN).opt etc # @echo " HELENA -u $(INPUT) (1 TIMES)" # $(H)rm -f etc/log.txt -# $(H)for T in `seq 1`; do ./$(MAIN).opt -T 1 -a n -l -m $(PREAMBLE) -o -u $(INPUT) >> etc/log.txt; done +# $(H)for T in `seq 1`; do ./$(MAIN).opt -T 1 -M $(OUTPUT) -a n -l -m $(PREAMBLE) -o -u $(INPUT) >> etc/log.txt; done # $(H)grep "at exit" etc/log.txt | sort | uniq > etc/profile-new.txt include Makefile.common diff --git a/helm/software/helena/Makefile.common b/helm/software/helena/Makefile.common index a601c4d88..1db6ea340 100644 --- a/helm/software/helena/Makefile.common +++ b/helm/software/helena/Makefile.common @@ -73,7 +73,7 @@ $(MAIN).opt: $(O_OBJECTS) $(H)$(OCAMLOPT) -o $(MAIN).opt $(CMXS) $(MAIN).byte: $(B_OBJECTS) - @echo " OCAMC -o $(MAIN).byte" + @echo " OCAMLC -o $(MAIN).byte" $(H)$(OCAMLC) -o $(MAIN).byte $(CMOS) .depend.opt: $(SOURCES) diff --git a/helm/software/helena/README b/helm/software/helena/README index 646b33526..37f553a25 100644 --- a/helm/software/helena/README +++ b/helm/software/helena/README @@ -9,20 +9,42 @@ SUMMARY enable option -d (if unset, -d is disabled) EXPAND enable option -g (if unset, -g is disabled) MANAGER enable options -M -m -p (if unset, -m is disabled) OBJECTS enable options -O -o (if unset, -o is disabled) -PREPROCESS enable option -p (if unset, -p is disabled) +PREPROCESS enable option -0 (if unset, -0 is disabled) QUOTE enable option -q (if unset, -q is disabled) TYPE enable option -t (if unset, -t is disabled) -* type "make opt" to compile the native executable - with the desired features listed in the variable F +* Type "make opt" to compile the native executable + with all features enabled + +* Type "make byte" to compile the bytecode executable + with all features enabled + +* Type "make" or "make all" to compile both executables + with all features enabled + +* Type "make clean" to remove the products of compilation -* type "make byte" to compile the bytecode executable +* Type "make ./helena.opt" to compile the native executable with the desired features listed in the variable F -* type "make" or "make all" to compile both executables +* Type "make ./helena.byte" to compile the bytecode executable with the desired features listed in the variable F -* type "make clean" to remove the products of compilation +* Set at least F="" for targets: + test-si-fast test1 test2-opt test2-byte profile-fast profile profile-opt profile-byte + +* Set at least F="TRACE" for targets: + test3 test6 + +* Set at least F="SUMMARY PREPROCESS" for targets: + test-si + +* Set at least F="OBJECTS QUOTE" for targets: + xml-si xml-si-v3 xml xml-v3 + +* Set at least F="MANAGER QUOTE" for targets: + export-coq export-matita export-lp1 export-lp2 export-tj2 export-tj3 -* type "make profile" to validate the "grundlagen" 31 times +* Type "make profile.opt" or "make profile.byte" + to validate the "grundlagen" 31 times (two runs each time) it generates etc/profile.txt with sorted execution times diff --git a/helm/software/helena/coq/grundlagen.template b/helm/software/helena/scripts/coq/grundlagen.template similarity index 100% rename from helm/software/helena/coq/grundlagen.template rename to helm/software/helena/scripts/coq/grundlagen.template diff --git a/helm/software/helena/coq/grundlagen_2.v b/helm/software/helena/scripts/coq/grundlagen_2.v similarity index 99% rename from helm/software/helena/coq/grundlagen_2.v rename to helm/software/helena/scripts/coq/grundlagen_2.v index 0d4f57cec..c86fab91e 100644 --- a/helm/software/helena/coq/grundlagen_2.v +++ b/helm/software/helena/scripts/coq/grundlagen_2.v @@ -9,7 +9,7 @@ (* *) (**************************************************************************) -(* This file was generated by Helena 0.8.3 M (June 2015): do not edit *****) +(* This file was generated by Helena 0.8.3 M (December 2015): do not edit *) (* constant 1 *) Definition l_imp := (fun (a:Prop) => (fun (b:Prop) => ((forall (x:a), b) : Prop))). diff --git a/helm/software/helena/coq/grundlagen_2_ver.v b/helm/software/helena/scripts/coq/grundlagen_2_ver.v similarity index 100% rename from helm/software/helena/coq/grundlagen_2_ver.v rename to helm/software/helena/scripts/coq/grundlagen_2_ver.v diff --git a/helm/software/helena/lp/lp.template b/helm/software/helena/scripts/lp/lp.template similarity index 100% rename from helm/software/helena/lp/lp.template rename to helm/software/helena/scripts/lp/lp.template diff --git a/helm/software/helena/matita/grundlagen_2.ma b/helm/software/helena/scripts/matita/grundlagen_2.ma similarity index 99% rename from helm/software/helena/matita/grundlagen_2.ma rename to helm/software/helena/scripts/matita/grundlagen_2.ma index 304439b02..f62c102b4 100644 --- a/helm/software/helena/matita/grundlagen_2.ma +++ b/helm/software/helena/scripts/matita/grundlagen_2.ma @@ -12,7 +12,7 @@ (* *) (**************************************************************************) -(* This file was generated by Helena 0.8.3 M (June 2015): do not edit *****) +(* This file was generated by Helena 0.8.3 M (December 2015): do not edit *) include "basics/pts.ma". diff --git a/helm/software/helena/matita/grundlagen_2_0.ma b/helm/software/helena/scripts/matita/grundlagen_2_0.ma similarity index 100% rename from helm/software/helena/matita/grundlagen_2_0.ma rename to helm/software/helena/scripts/matita/grundlagen_2_0.ma diff --git a/helm/software/helena/matita/grundlagen_2_1.ma b/helm/software/helena/scripts/matita/grundlagen_2_1.ma similarity index 100% rename from helm/software/helena/matita/grundlagen_2_1.ma rename to helm/software/helena/scripts/matita/grundlagen_2_1.ma diff --git a/helm/software/helena/matita/grundlagen_2_2.ma b/helm/software/helena/scripts/matita/grundlagen_2_2.ma similarity index 100% rename from helm/software/helena/matita/grundlagen_2_2.ma rename to helm/software/helena/scripts/matita/grundlagen_2_2.ma diff --git a/helm/software/helena/matita/grundlagen_2_3.ma b/helm/software/helena/scripts/matita/grundlagen_2_3.ma similarity index 100% rename from helm/software/helena/matita/grundlagen_2_3.ma rename to helm/software/helena/scripts/matita/grundlagen_2_3.ma diff --git a/helm/software/helena/matita/grundlagen_2_4.ma b/helm/software/helena/scripts/matita/grundlagen_2_4.ma similarity index 100% rename from helm/software/helena/matita/grundlagen_2_4.ma rename to helm/software/helena/scripts/matita/grundlagen_2_4.ma diff --git a/helm/software/helena/matita/grundlagen_2_5.ma b/helm/software/helena/scripts/matita/grundlagen_2_5.ma similarity index 100% rename from helm/software/helena/matita/grundlagen_2_5.ma rename to helm/software/helena/scripts/matita/grundlagen_2_5.ma diff --git a/helm/software/helena/matita/grundlagen_2_6.ma b/helm/software/helena/scripts/matita/grundlagen_2_6.ma similarity index 100% rename from helm/software/helena/matita/grundlagen_2_6.ma rename to helm/software/helena/scripts/matita/grundlagen_2_6.ma diff --git a/helm/software/helena/matita/root b/helm/software/helena/scripts/matita/root similarity index 100% rename from helm/software/helena/matita/root rename to helm/software/helena/scripts/matita/root diff --git a/helm/software/helena/src/automath/autLexer.mll b/helm/software/helena/src/automath/autLexer.mll index 5a7155e4a..58324a021 100644 --- a/helm/software/helena/src/automath/autLexer.mll +++ b/helm/software/helena/src/automath/autLexer.mll @@ -10,6 +10,8 @@ V_______________________________________________________________ *) { + module KT = String + module L = Log module G = Options module AP = AutParser @@ -23,15 +25,12 @@ END IFDEF QUOTE THEN (* This turns an Automath identifier into an XML nmtoken *) let quote id = - let l = String.length id in - let rec aux i = - if i < l then begin - if id.[i] = '\'' || id.[i] = '`' then id.[i] <- '_'; - aux (succ i) - end else - id + let map = function + | '\'' + | '`' -> '_'; + | c -> c in - aux 0 + KT.map map id END } diff --git a/helm/software/helena/src/basic_rg/brgReduction.ml b/helm/software/helena/src/basic_rg/brgReduction.ml index e62b90777..4a9570d50 100644 --- a/helm/software/helena/src/basic_rg/brgReduction.ml +++ b/helm/software/helena/src/basic_rg/brgReduction.ml @@ -10,6 +10,7 @@ V_______________________________________________________________ *) module U = NUri +module C = Cps module S = Share module L = Log module G = Options @@ -44,10 +45,11 @@ let log2 st s cu u ct t = let s1, s2, s3 = s ^ " in the environment (expected)", "the term", "and in the environment (inferred)" in L.log st BO.specs (pred level) (L.et_items2 s1 cu s2 u ~sc2:s3 ~c2:ct s2 t) -let rec list_and map = function +let rec list_and f map = function | hd1 :: tl1, hd2 :: tl2 -> - if map hd1 hd2 then list_and map (tl1, tl2) else false - | l1, l2 -> l1 = l2 + let f b = f (b && map hd1 hd2) in + list_and f map (tl1, tl2) + | l1, l2 -> f (l1 = l2) let zero = Some 0 @@ -258,12 +260,11 @@ and ac st m1 t1 m2 t2 = and ac_stacks st m1 m2 = (* L.warn "entering R.are_convertible_stacks"; *) - if List.length m1.s <> List.length m2.s then false else let map (c1, v1) (c2, v2) = let m1, m2 = reset m1 ~e:c1 zero, reset m2 ~e:c2 zero in ac st m1 v1 m2 v2 in - list_and map (m1.s, m2.s) + list_and C.start map (m1.s, m2.s) let rec ih_nfs st (m, t, r) = match t, r with diff --git a/helm/software/helena/src/common/options.ml b/helm/software/helena/src/common/options.ml index dfbf27d41..f268ba344 100644 --- a/helm/software/helena/src/common/options.ml +++ b/helm/software/helena/src/common/options.ml @@ -32,8 +32,8 @@ END (* interface functions ******************************************************) let version_string b = - if b then "Helena 0.8.3 M (July 2015)" - else "Helena 0.8.3 M - July 2015" + if b then "Helena 0.8.3 M (December 2015)" + else "Helena 0.8.3 M - December 2015" let kernel = ref V3 (* kernel type *) @@ -101,7 +101,7 @@ let preprocess = ref false (* preprocess source *) END IFDEF QUOTE THEN -let quote = ref false (* quote identifiers when lexing *) +let quote = ref false (* quote identifiers when lexing *) END IFDEF TYPE THEN -- 2.39.2