From f438e9b0c8e43a66c56b17adeb8793042d0aade1 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Tue, 29 May 2007 15:30:53 +0000
Subject: [PATCH] added some lines to compile for debugging

---
 helm/software/components/Makefile.common             | 6 ++++--
 helm/software/components/cic_proof_checking/cicPp.ml | 2 +-
 helm/software/components/tactics/Makefile            | 2 ++
 helm/software/components/tactics/auto.ml             | 2 +-
 helm/software/components/tactics/tacticals.ml        | 2 +-
 helm/software/matita/Makefile                        | 3 ++-
 6 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/helm/software/components/Makefile.common b/helm/software/components/Makefile.common
index 30bd4c889..59b35aa73 100644
--- 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 d065ee74a..8c37c0f93 100644
--- 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 899081299..e6f63eac0 100644
--- 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 4cd6bf62f..e42c3ba51 100644
--- 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 f3f779303..06f96a573 100644
--- 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 444febcae..97158f9dd 100644
--- 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
-- 
2.39.2