nelim now uses the appropriate _rect_XXX elimination principle

[helm.git] / helm / software / components / ng_tactics / nCicElim.ml

diff --git a/helm/software/components/ng_tactics/nCicElim.ml b/helm/software/components/ng_tactics/nCicElim.ml
index 350144f9e430307d5983f56a0590d9d1fa936de2..ae472ae38cbdaf37633b73fe2655342d589fa1bc 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 =
@@ -107,15 +106,17 @@ let mk_elim uri leftno [it] (outsort,suffix) =
      let cargs,recursive_args = List.split cargs_and_recursive_args in
      let recursive_args = HExtlib.filter_map (fun x -> x) recursive_args in
       CicNotationPt.Pattern (name,None,List.map (fun x -> x,None) cargs),
-       CicNotationPt.Appl (name_of_k name :: cargs @ recursive_args)
+       mk_appl (name_of_k name :: cargs @ recursive_args)
    ) cl
  in
- let bo = CicNotationPt.Case (rec_arg,None,None,branches) in
- let where = List.length final_params - 1 in
+ let bo = CicNotationPt.Case (rec_arg,Some (ind_name,None),None,branches) 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)
 ;;