From bc4a1cafaf3ffa471483210da7b076feeed7c0dc Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sat, 26 Dec 2015 18:57:21 +0000
Subject: [PATCH] bug fixes ...

---
 helm/software/helena/Makefile                   | 4 ++--
 helm/software/helena/Makefile.common            | 7 ++-----
 helm/software/helena/src/basic_rg/brgGallina.ml | 2 +-
 3 files changed, 5 insertions(+), 8 deletions(-)

diff --git a/helm/software/helena/Makefile b/helm/software/helena/Makefile
index e21fccf1b..48f7e4b96 100644
--- a/helm/software/helena/Makefile
+++ b/helm/software/helena/Makefile
@@ -17,8 +17,6 @@ TAGS = test-si-fast test-si test2-opt test2-byte test3 test6 \
        export-lp1 export-lp2 export-tj2 export-tj3 \
        matita matitac
 
-include Makefile.common
-
 TIME = `which time` -p -a -o etc/log.txt
 
 NULL = >/dev/null 2>&1 
@@ -179,3 +177,5 @@ matitac: matita/$(MA)
 #	$(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)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 ae92e7df6..a601c4d88 100644
--- a/helm/software/helena/Makefile.common
+++ b/helm/software/helena/Makefile.common
@@ -1,9 +1,6 @@
 H=@
-ifeq ($(origin OCAMLPATH), undefined)
-   OCAMLFIND = OCAMLPATH=$(HOME)/svn/claudio/components/METAS ocamlfind
-else
-   OCAMLFIND = ocamlfind
-endif
+OCAMLPATH ?= /home/fguidi/svn/matita_patched/components/METAS
+OCAMLFIND = OCAMLPATH=$(OCAMLPATH) ocamlfind
 
 RELISE = $(MAIN:%=%_$(shell cat MakeVersion))
 
diff --git a/helm/software/helena/src/basic_rg/brgGallina.ml b/helm/software/helena/src/basic_rg/brgGallina.ml
index 100b7c4df..7346e5835 100644
--- a/helm/software/helena/src/basic_rg/brgGallina.ml
+++ b/helm/software/helena/src/basic_rg/brgGallina.ml
@@ -124,7 +124,7 @@ let output_entity och st (_, na, u, b) =
          KP.fprintf och "exact %a.\n%!" (out_term st true B.empty) v;
          KP.fprintf och "Time Defined.\n\n%!";
 *)
-      | E.Abbr V ->
+      | E.Abbr v ->
          KP.fprintf och "Definition %a := %a.\n\n%!" out_uri u (out_term st false B.empty) v;
 (*         KP.fprintf och "Strategy -%u [ %a ].\n\n%!" na.E.n_apix out_uri u; *) !ok
       | E.Abst w ->
-- 
2.39.2