From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Fri, 17 Jul 2009 14:05:29 +0000 (+0000)
Subject: Debugging code commented out.
X-Git-Tag: make_still_working~3665
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=b939bfdb17f3ce464c31db7463586d5f88a9700c;p=helm.git

Debugging code commented out.
---

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 0c1a98ec3..1401ed48f 100644
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -66,7 +66,6 @@ let mk_elim uri leftno [it] (outsort,suffix) =
   [p_name,Some p_ty] @
   List.map (function name -> name, None) k_names @
   List.map (function name -> name, None) args in
- let recno = List.length final_params in
  let cty = mk_appl (p_name :: args) in
  let ty = Some cty in
  let branches =
@@ -111,11 +110,13 @@ let mk_elim uri leftno [it] (outsort,suffix) =
    ) cl
  in
  let bo = CicNotationPt.Case (rec_arg,None,None,branches) in
- let where = List.length final_params - 1 in
+ let recno = List.length final_params in
+ let where = recno - 1 in
  let res =
   CicNotationPt.LetRec (`Inductive,
    [final_params, (rec_name,ty), bo, where], rec_name)
  in
+(*
   prerr_endline
    (BoxPp.render_to_string
      ~map_unicode_to_tex:false
@@ -146,6 +147,7 @@ let mk_elim uri leftno [it] (outsort,suffix) =
    (BoxPp.render_to_string ~map_unicode_to_tex:false
      (function x::_ -> x | _ -> assert false) 80 
      (CicNotationPres.mpres_of_box boxml)));
+*)
   CicNotationPt.Theorem (`Definition,srec_name,CicNotationPt.Implicit,Some res)
 ;;