repeat_tac

[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 54d8d5df62cfd27e2d9a28e862943fd5e1553c10..fba21753a53ce6ef8b749839b716020ca7b702e8 100644 (file)
--- a/helm/software/components/ng_tactics/nCicElim.ml
+++ b/helm/software/components/ng_tactics/nCicElim.ml
@@ -45,8 +45,8 @@ let mk_elims (uri,_,_,_,obj) =
      let params,ty = NCicReduction.split_prods ~subst:[] [] leftno ty in
      let params = List.rev_map (function name,_ -> mk_id name) params in
      let args,sort = NCicReduction.split_prods ~subst:[] [] (-1) ty in
-     let rec_arg = mk_id (fresh_name ()) in
      let args = List.rev_map (function name,_ -> mk_id name) args in
+     let rec_arg = mk_id (fresh_name ()) in
      let p_ty =
       List.fold_right
        (fun name res -> CicNotationPt.Binder (`Forall,(name,None),res)) args
@@ -70,23 +70,32 @@ let mk_elims (uri,_,_,_,obj) =
          let cargs_and_recursive_args =
           List.rev_map
            (function
-               name,NCic.Def _ -> assert false
-             | name,NCic.Decl (NCic.Const nref)
-             | name,NCic.Decl (NCic.Appl (NCic.Const nref::_))
-               when
-                let NReference.Ref (uri',_) = nref in
-                 NUri.eq uri uri'
-               ->
-                let name = mk_id name in
-                 name, Some (
-                 CicNotationPt.Appl
-                  (rec_name ::
-                   params @
-                   [p_name] @
-                   k_names @
-                   List.map (fun _ -> CicNotationPt.Implicit) (List.tl args) @
-                   [name]))
-             | name,_ -> mk_id name,None
+               _,NCic.Def _ -> assert false
+             | name,NCic.Decl ty ->
+                let context,ty = my_split_prods ~subst:[] [] (-1) ty in
+                 match ty with
+                  | NCic.Const nref
+                  | NCic.Appl (NCic.Const nref::_)
+                     when
+                      let NReference.Ref (uri',_) = nref in
+                       NUri.eq uri uri'
+                     ->
+                      let abs = List.rev_map (fun id,_ -> mk_id id) context in
+                      let name = mk_id name in
+                       name, Some (
+                       List.fold_right
+                        (fun id res ->
+                          CicNotationPt.Binder (`Lambda,(id,None),res))
+                        abs
+                        (CicNotationPt.Appl
+                         (rec_name ::
+                          params @
+                          [p_name] @
+                          k_names @
+                          List.map (fun _ -> CicNotationPt.Implicit)
+                           (List.tl args) @
+                          [CicNotationPt.Appl (name::abs)])))
+                  | _ -> mk_id name,None
            ) cargs in
          let cargs,recursive_args = List.split cargs_and_recursive_args in
          let recursive_args = HExtlib.filter_map (fun x -> x) recursive_args in
@@ -106,9 +115,8 @@ let mk_elims (uri,_,_,_,obj) =
        (BoxPp.render_to_string
          ~map_unicode_to_tex:false
          (function x::_ -> x | _ -> assert false)
-         80 (CicNotationPres.render (Hashtbl.create 0)
+         80 (CicNotationPres.render (fun _ -> None)
          (TermContentPres.pp_ast res)));
-
       []
   | _ -> []
 ;;