Patch to avoid equations of the form ? -> T (oriented this way) that

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

diff --git a/matita/components/ng_tactics/nCicElim.ml b/matita/components/ng_tactics/nCicElim.ml
index a41e2fb349f0cb31b39ceda6f463116c64324e7b..24fd7d8e9aa0eb65104e4bc7154632985f1e0d39 100644 (file)
--- a/matita/components/ng_tactics/nCicElim.ml
+++ b/matita/components/ng_tactics/nCicElim.ml
@@ -116,7 +116,7 @@ let mk_elim status uri leftno it (outsort,suffix) pragma =
    ) cl
  in
  let branches, branch_args = List.split branches_with_args in
- let bo = NotationPt.Case (rec_arg,Some (ind_name,None),None,branches) in
+ let bo = NotationPt.Case (rec_arg,Some (ind_name,None),Some p_name,branches) in
  let final_params =
   List.map (function name -> name, None) params @
   [p_name,Some p_ty] @