From ea3b15fdedb39c72ae1b39f210917c6f38fc062d Mon Sep 17 00:00:00 2001
From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 26 Sep 2008 15:03:55 +0000
Subject: [PATCH] Procedural: we removed some commented code matita/Makefile:
 tests re-enabled character: scheduled for daily testing

---
 .../acic_procedural/acic2Procedural.ml        | 20 +++----------------
 helm/software/matita/Makefile                 | 19 +++++++++---------
 helm/software/matita/contribs/Makefile        |  2 +-
 .../matita/contribs/character/Makefile        | 16 ++++++++-------
 4 files changed, 23 insertions(+), 34 deletions(-)

diff --git a/helm/software/components/acic_procedural/acic2Procedural.ml b/helm/software/components/acic_procedural/acic2Procedural.ml
index 071377c63..253162009 100644
--- a/helm/software/components/acic_procedural/acic2Procedural.ml
+++ b/helm/software/components/acic_procedural/acic2Procedural.ml
@@ -221,18 +221,6 @@ let convert st ?name v =
       | None            -> 
          if !debug then [T.Note "NORMAL: NO INNER TYPES"] else []
       | Some (sty, ety) -> mk_convert st ?name sty ety "NORMAL"
-
-let convert_elim st ?name t v pattern =
-   match t, get_inner_types st t, get_inner_types st v with
-      | _, None, _
-      | _, _, None                                            -> [(* T.Note "ELIM: NO INNER TYPES"*)]
-      | C.AAppl (_, hd :: tl), Some (tsty, _), Some (vsty, _) ->
-         let where = List.hd (List.rev tl) in
-         let cty = Cn.elim_inferred_type 
-	     st.context (H.cic vsty) (H.cic where) (H.cic hd) (H.cic pattern)
-	 in
-         mk_convert st ?name (Cn.fake_annotate "" st.context cty) tsty "ELIM"
-      | _, Some _, Some _                                     -> assert false
 	  
 let get_intro = function 
    | C.Anonymous -> None
@@ -256,10 +244,9 @@ let mk_fwd_rewrite st dtext name tl direction v t ity =
    if (Cn.does_not_occur e) then st, [] else 
    match where with
       | C.ARel (_, _, i, premise) as w ->
-(*         let _script = convert_elim st ~name:(premise, i) v w e in *) 
          let script name =
             let where = Some (premise, name) in
-	    let script = mk_arg st what @ mk_arg st w (* @ script *) in
+	    let script = mk_arg st what @ mk_arg st w in
 	    T.Rewrite (direction, what, where, e, dtext) :: script
 	 in
 	 if DTI.does_not_occur (succ i) (H.cic t) || compare premise name then
@@ -279,8 +266,7 @@ let mk_rewrite st dtext where qs tl direction t =
    let predicate = List.nth tl 2 in
    let e = Cn.mk_pattern 1 predicate in
    let script = [T.Branch (qs, "")] in
-   if (Cn.does_not_occur e) then script else 
-(*   let script = convert_elim st t t e in *)
+   if (Cn.does_not_occur e) then script else
    T.Rewrite (direction, where, None, e, dtext) :: script
 
 let rec proc_lambda st what name v t =
@@ -382,7 +368,7 @@ and proc_appl st what hd tl =
 	       let predicate = List.nth tl2 (parsno - i) in
                let e = Cn.mk_pattern j predicate in
 	       let using = Some hd in
-	       (* convert_elim st what what e @ *) script2 @ 
+	       script2 @ 
 	       [T.Elim (where, using, e, dtext ^ text); T.Branch (qs, "")]
 	 | None        ->
 	    let names = get_sub_names hd tl in
diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile
index 8bd708eb7..1f9bff299 100644
--- a/helm/software/matita/Makefile
+++ b/helm/software/matita/Makefile
@@ -181,21 +181,22 @@ distclean: clean
 
 TEST_DIRS = 				\
 	legacy                          \
-	library 			
-	# tests 				\
-	# contribs/dama/dama		\
-	# contribs/assembly		\
-	# contribs/CoRN	 	        \
-	# contribs/RELATIONAL	 	\
-	# contribs/LOGIC	       	 	\
-	# contribs/PREDICATIVE-TOPOLOGY 	\
+	library 			\
+	contribs/character              \
+	tests 			        \
+	contribs/dama/dama		\
+	contribs/assembly		\
+	contribs/CoRN	 	        \
+	contribs/RELATIONAL	 	\
+	contribs/LOGIC	       	        \
+	contribs/PREDICATIVE-TOPOLOGY   \
 	$(NULL)
 
 #	library_auto 			
 TEST_DIRS_OPT = 			\
 	$(TEST_DIRS)                    \
+	# contribs/LAMBDA-TYPES 	\
 	$(NULL)
-	#contribs/LAMBDA-TYPES 		\
 
 .PHONY: tests tests.opt cleantests cleantests.opt
 tests: $(foreach d,$(TEST_DIRS),$(d)-test)
diff --git a/helm/software/matita/contribs/Makefile b/helm/software/matita/contribs/Makefile
index 8c2e0647a..2a4ae4bfc 100644
--- a/helm/software/matita/contribs/Makefile
+++ b/helm/software/matita/contribs/Makefile
@@ -1,6 +1,6 @@
 GOALS = all opt clean clean.opt
 
-DEVELS = RELATIONAL LOGIC LAMBDA-TYPES assembly dama POPLmark CoRN
+DEVELS = RELATIONAL LOGIC LAMBDA-TYPES assembly dama POPLmark CoRN character
 
 $(GOALS): 
 	@$(foreach DEVEL, $(DEVELS), $(MAKE) -C $(DEVEL) $@;) 
diff --git a/helm/software/matita/contribs/character/Makefile b/helm/software/matita/contribs/character/Makefile
index a3e891435..8262cd704 100644
--- a/helm/software/matita/contribs/character/Makefile
+++ b/helm/software/matita/contribs/character/Makefile
@@ -1,16 +1,18 @@
-include ../Makefile.defs
+BIN=../../
 
 DIR=$(shell basename $$PWD)
 
+H=@
+
 $(DIR) all:
-	$(BIN)matitac
+	$(H)$(BIN)matitac
 $(DIR).opt opt all.opt:
-	$(BIN)matitac.opt
+	$(H)$(BIN)matitac.opt
 clean:
-	$(BIN)matitaclean
+	$(H)$(BIN)matitaclean
 clean.opt:
-	$(BIN)matitaclean.opt
+	$(H)$(BIN)matitaclean.opt
 depend:
-	$(BIN)matitadep
+	$(H)$(BIN)matitadep
 depend.opt:
-	$(BIN)matitadep.opt
+	$(H)$(BIN)matitadep.opt
-- 
2.39.2