From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Wed, 11 Mar 2009 15:37:54 +0000 (+0000)
Subject: Procedural: id tactics are not counted, ie they are placeholders
X-Git-Tag: make_still_working~4155
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=becc738132009807d8e056734cf78ace63213592;p=helm.git

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 b7f3e31b9..cb4c11d2e 100644
--- 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 fef14b2b8..3e42a4ea1 100644
--- 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 65346b508..d205172eb 100644
--- 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