Procedural: id tactics are not counted, ie they are placeholders

LAMBDA-TYPES: bugfix in depend +
              makefile entries for %.ma %.mma %.ma.opt %.mma.opt

diff --git a/helm/software/components/acic_procedural/proceduralTypes.ml b/helm/software/components/acic_procedural/proceduralTypes.ml
index b7f3e31b9f87b2cf9fc6ded31f63c350152331b9..cb4c11d2ee6f87b10d671297b936f903a4da36a4 100644 (file)
--- a/helm/software/components/acic_procedural/proceduralTypes.ml
+++ b/helm/software/components/acic_procedural/proceduralTypes.ml
@@ -274,6 +274,7 @@ let render_steps a = render_steps mk_dot a
 let rec count_step a = function
    | Note _
    | Statement _  
+   | Id _
    | Qed _           -> a
    | Branch (pps, _) -> List.fold_left count_steps a pps
    | _               -> succ a   

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
index fef14b2b888584258cffccf0ee41955d14617cd2..3e42a4ea18c5fd0fd93d5b0a149b47c6009aef07 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/Makefile
@@ -17,12 +17,24 @@ $(DIR) all:
 $(DIR).opt opt all.opt:
        $(H)$(RM) $(LOG)
        $(H)$(BIN)matitac.opt $(MATITAOPTIONS) 2>> $(LOG)
+
+%.ma %.mma: 
+       $(H)$(RM) $(LOG)
+       $(H)$(BIN)matitac $(MATITAOPTIONS) $@ 2>> $(LOG)
+%.ma.opt: 
+       $(H)$(RM) $(LOG)
+       $(H)$(BIN)matitac.opt $(MATITAOPTIONS) $*.ma 2>> $(LOG)
+%.mma.opt: 
+       $(H)$(RM) $(LOG)
+       $(H)$(BIN)matitac.opt $(MATITAOPTIONS) $*.mma 2>> $(LOG)
+
 clean:
        $(H)$(BIN)matitaclean $(MATITAOPTIONS)
        $(H)$(RM) $(MAS)
 clean.opt:
        $(H)$(BIN)matitaclean.opt $(MATITAOPTIONS)
        $(H)$(RM) $(MAS)
+
 depend:
        $$(H)(BIN)matitadep $(MATITAOPTIONS)
 depend.opt:

diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/depends b/helm/software/matita/contribs/LAMBDA-TYPES/depends
index 65346b5083f7a1e47ce7a29ea0886379c556cb49..d205172eb1b68b1b0eb0d48325eeecacac8bbd63 100644 (file)
--- a/helm/software/matita/contribs/LAMBDA-TYPES/depends
+++ b/helm/software/matita/contribs/LAMBDA-TYPES/depends
@@ -204,7 +204,7 @@ Basic-2/nf2/arity.ma Basic-2/nf2/arity.mma
 Basic-1/ty3/subst1.ma Basic-1/getl/getl.ma Basic-1/pc3/subst1.ma Basic-1/ty3/props.ma
 Basic-2/subst0/fwd.mma Basic-1/subst0/fwd.ma Basic-2/lift/props.ma Basic-2/subst0/defs.ma
 Basic-2/pc1/props.mma Basic-1/pc1/props.ma Basic-2/pc1/defs.ma Basic-2/pr1/pr1.ma
-Legacy-2/preamble.ma Legacy-1/preamble.ma Legacy-1/coq/defs.ma Legacy-1/coq/props.ma Legacy-1/definitions.ma
+Legacy-2/preamble.ma Legacy-1/preamble.ma Legacy-1/coq/defs.ma Legacy-1/coq/props.ma Legacy-1/theory.ma
 Basic-2/csuba/drop.mma Basic-1/csuba/drop.ma Basic-2/csuba/fwd.ma Basic-2/drop/fwd.ma
 Basic-2/csubc/fwd.mma Basic-1/csubc/fwd.ma Basic-2/csubc/defs.ma
 Basic-1/csubc/csuba.ma Basic-1/csubc/defs.ma Basic-1/sc3/props.ma