- grafiteParser.ml: the callback invocation was displaced

- cicNotationPres.ml: hack to have more brackets because
  (forall .. \to ..) was rendered without brackets. FIXME!
- LAMBDA-TYPES: improved Makefile

diff --git a/helm/software/components/content_pres/cicNotationPres.ml b/helm/software/components/content_pres/cicNotationPres.ml
index 84eaaeb2a7711dd85e7d898294de6729f9a5913c..175aae993aca95e502196319f4db119d6388b5cf 100644 (file)
--- a/helm/software/components/content_pres/cicNotationPres.ml
+++ b/helm/software/components/content_pres/cicNotationPres.ml
@@ -188,7 +188,8 @@ let add_parens child_prec curr_prec t =
     child_prec (pp_assoc child_assoc) (CicNotationPp.pp_pos child_pos)
     curr_prec; *)
   if is_atomic t then t
-  else if child_prec >= 0 && child_prec < curr_prec then 
+(* FG: FIXME: should be < but < causes no brackets when \forall .. \to .. associates to the left *)  
+  else if child_prec >= 0 && child_prec <= curr_prec then 
     begin (* parens should be added *)
 (*      prerr_endline "adding parens!";  *)
     match t with

diff --git a/helm/software/components/grafite_parser/grafiteParser.ml b/helm/software/components/grafite_parser/grafiteParser.ml
index 18c30d4ecbddcfa141c229131223d6c8149f3761..20aad1cd3a19c16788264e634cb95028cca31c89 100644 (file)
--- a/helm/software/components/grafite_parser/grafiteParser.ml
+++ b/helm/software/components/grafite_parser/grafiteParser.ml
@@ -711,6 +711,7 @@ EXTEND
     | com = comment ->
        fun ?(never_include=false) ~include_paths status -> status,LSome (GrafiteAst.Comment (loc, com))
     | (iloc,fname,mode) = include_command ; SYMBOL "."  ->
+       !out fname;       
        fun ?(never_include=false) ~include_paths status ->
         let _root, buri, fullpath, _rrelpath = 
           Librarian.baseuri_of_script ~include_paths fname 
@@ -720,7 +721,6 @@ EXTEND
          else LexiconEngine.eval_command status 
                 (LexiconAst.Include (iloc,buri,mode,fullpath))
         in
-         !out fname;
          status,
           LSome
           (GrafiteAst.Executable

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
index fb55d67825a0e66712a1a6e783b68115692d1eeb..9608434b6afc4f115a1e431456bada8527380578 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
@@ -6,27 +6,31 @@ MATITAOPTIONS=$(MATITAUSEROPTIONS) -onepass
 
 DIR=$(shell basename $$PWD)
 
+LOG = log.txt
+
 MMAS = $(shell find Legacy-2 Base-2 -name "*.mma") 
 MAS = $(MMAS:%.mma=%.ma)
 XMAS = Legacy-2/theory.ma Base-2/theory.ma LambdaDelta-2/theory.ma
 
 $(DIR) all: depends
+       $(H)$(RM) $(LOG)
        $(H)$(MAKE) H=$(H) --no-print-directory build
 
 $(DIR).opt opt all.opt: depends
+       $(H)$(RM) $(LOG)
        $(H)$(MAKE) H=$(H) --no-print-directory build.opt
 
 build: $(MAS)
        $(H)echo Legacy-2/theory.ma `$(BIN)matitadep.opt -stdout Legacy-2/theory.ma` >> depends
        $(H)echo Base-2/theory.ma `$(BIN)matitadep.opt -stdout Base-2/theory.ma` >> depends
-       $(H)$(BIN)matitac $(MATITAOPTIONS) 2> /dev/null
-       $(H)rm depends
+       $(H)$(BIN)matitac $(MATITAOPTIONS) 2>> $(LOG)
+       $(H)$(RM) depends
 
 build.opt: $(MAS)
        $(H)echo Legacy-2/theory.ma `$(BIN)matitadep.opt -stdout Legacy-2/theory.ma` >> depends
        $(H)echo Base-2/theory.ma `$(BIN)matitadep.opt -stdout Base-2/theory.ma` >> depends
-       $(H)$(BIN)matitac.opt $(MATITAOPTIONS) 2> /dev/null
-       $(H)rm depends
+       $(H)$(BIN)matitac.opt $(MATITAOPTIONS) 2>> $(LOG)
+       $(H)$(RM) depends
 
 clean:
        $(H)$(BIN)matitaclean $(MATITAOPTIONS)
@@ -53,8 +57,8 @@ depend.opt:
 depends: depend.opt
 
 %.ma: %.mma
-       $(H)$(BIN)matitac.opt $(MATITAOPTIONS) $(word 3,$(shell grep -h $< */depends)) `$(BIN)matitadep.opt -stdout $<` 2> /dev/null
-       $(H)$(BIN)matitac.opt $(MATITAOPTIONS) -dump $@ $< 2> /dev/null
+       $(H)$(BIN)matitac.opt $(MATITAOPTIONS) $(word 3,$(shell grep -h $< */depends)) `$(BIN)matitadep.opt -stdout $<` 2>> $(LOG)
+       $(H)$(BIN)matitac.opt $(MATITAOPTIONS) -dump $@ $< 2>> $(LOG)
        $(H)echo $@ `$(BIN)matitadep.opt -stdout $@` >> depends
 
 include Legacy-2/.depend