Debugging code commented out.

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 0c1a98ec342a9848406f925bc60056257afa1a59..1401ed48f8b6ecc7fe9849e02496a8fb62428031 100644 (file)
--- 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)
 ;;