added some lines to compile for debugging

diff --git a/helm/software/components/Makefile.common b/helm/software/components/Makefile.common
index 30bd4c8898b29c533655d94ddc5553ed9d908624..59b35aa7371348377d34bd9d6b4735169b708165 100644 (file)
--- a/helm/software/components/Makefile.common
+++ b/helm/software/components/Makefile.common
@@ -16,10 +16,12 @@ SYNTAXOPTIONS = -syntax camlp4o
 PREREQ =
 OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -thread
 OCAMLDEBUGOPTIONS = -g
+#OCAML_PROF=p -p a
 OCAMLARCHIVEOPTIONS =
 REQUIRES := $(shell $(OCAMLFIND) -query -format '%(requires)' helm-$(PACKAGE))
-OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) $(PREPROCOPTIONS)
-OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) $(PREPROCOPTIONS)
+OCAMLC = $(OCAMLFIND) ocamlc$(OCAML_PROF) $(OCAMLDEBUGOPTIONS) $(OCAMLOPTIONS) $(PREPROCOPTIONS)
+#OCAMLOPT_DEBUG_FLAGS = -p
+OCAMLOPT = $(OCAMLFIND) opt $(OCAMLOPTIONS) $(PREPROCOPTIONS) $(OCAMLOPT_DEBUG_FLAGS)
 OCAMLDEP = $(OCAMLFIND) ocamldep -package "camlp4 $(CAMLP4REQUIRES)" $(SYNTAXOPTIONS) $(OCAMLDEPOPTIONS) 
 OCAMLLEX = ocamllex
 OCAMLYACC = ocamlyacc

diff --git a/helm/software/components/cic_proof_checking/cicPp.ml b/helm/software/components/cic_proof_checking/cicPp.ml
index d065ee74a0d04c4d13a0f40dd6372d92c0dadcb8..8c37c0f939f8aeed9d0f29999c7b8233f88f5147 100644 (file)
--- a/helm/software/components/cic_proof_checking/cicPp.ml
+++ b/helm/software/components/cic_proof_checking/cicPp.ml
@@ -167,7 +167,7 @@ let rec pp t l =
             C.InductiveDefinition (dl,_,paramsno,_) ->
              let (_,_,_,cons) = get_nth dl (n1+1) in
               List.map
-               (fun id,ty ->
+               (fun (id,ty) ->
                  (* this is just an approximation since we do not have
                     reduction yet! *)
                  let rec count_prods toskip =

diff --git a/helm/software/components/tactics/Makefile b/helm/software/components/tactics/Makefile
index 8990812993d9e897b9a88761ea8e286e69fec930..e6f63eac0a5ee0e9e28018d161f1a1b5efc84c38 100644 (file)
--- a/helm/software/components/tactics/Makefile
+++ b/helm/software/components/tactics/Makefile
@@ -56,3 +56,5 @@ include ../Makefile.common
 
 OCAMLOPTIONS+= -I paramodulation
 OCAMLDEPOPTIONS+= -I paramodulation
+#PREPROCOPTIONS:=
+#OCAML_PROF=p -p a

diff --git a/helm/software/components/tactics/auto.ml b/helm/software/components/tactics/auto.ml
index 4cd6bf62ff477db6033aafcd9eeb9e82871fbbe8..e42c3ba513ed2d9e1e1993616f1336337f2a9f56 100644 (file)
--- a/helm/software/components/tactics/auto.ml
+++ b/helm/software/components/tactics/auto.ml
@@ -1085,7 +1085,7 @@ let equational_case
         assert (maxmeta >= maxm);
         let res' =
           List.map 
-            (fun subst',(_,metasenv,_subst,proof,_, _),open_goals ->
+            (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
                assert_subst_are_disjoint subst subst';
                let subst = subst@subst' in
                let open_goals = 

diff --git a/helm/software/components/tactics/tacticals.ml b/helm/software/components/tactics/tacticals.ml
index f3f7793032365bb5194137002b9356e0a2a80881..06f96a573c28f367c244a649080c4fc136c7e981 100644 (file)
--- a/helm/software/components/tactics/tacticals.ml
+++ b/helm/software/components/tactics/tacticals.ml
@@ -113,7 +113,7 @@ struct
      back to obtain the result of the tactic *)
   let mk_tactic f =
     PET.mk_tactic
-      (fun (proof, goal) as pstatus ->
+      (fun ((proof, goal) as pstatus) ->
         let stack = [ [ 1, Stack.Open goal ], [], [], `NoTag ] in
         let istatus = pstatus, stack in
         let (proof, _, _), stack = f istatus in

diff --git a/helm/software/matita/Makefile b/helm/software/matita/Makefile
index 444febcae67301c924373c956e35e9ac71e2fce1..97158f9dd566a7c997380b51dd162f60978f58d4 100644 (file)
--- a/helm/software/matita/Makefile
+++ b/helm/software/matita/Makefile
@@ -10,9 +10,10 @@ PKGS = -package "$(MATITA_REQUIRES)"
 CPKGS = -package "$(MATITA_CREQUIRES)"
 OCAML_THREADS_FLAGS = -thread
 OCAML_DEBUG_FLAGS = -g
+#OCAML_PROF=p -p a
 #OCAMLOPT_DEBUG_FLAGS = -p
 OCAMLC_FLAGS = $(OCAML_FLAGS) $(OCAML_THREADS_FLAGS)
-OCAMLC = $(OCAMLFIND) ocamlc $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS)
+OCAMLC = $(OCAMLFIND) ocamlc$(OCAML_PROF) $(OCAMLC_FLAGS) $(OCAML_DEBUG_FLAGS)
 OCAMLOPT = $(OCAMLFIND) opt $(OCAMLC_FLAGS) $(OCAMLOPT_DEBUG_FLAGS)
 OCAMLDEP = $(OCAMLFIND) ocamldep $(OCAML_FLAGS)
 INSTALL_PROGRAMS= matita matitac