From b939bfdb17f3ce464c31db7463586d5f88a9700c Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Fri, 17 Jul 2009 14:05:29 +0000 Subject: [PATCH] Debugging code commented out. --- helm/software/components/ng_tactics/nCicElim.ml | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) 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) ;; -- 2.39.2