X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnInversion.ml;h=f1da10cb7a08c3ab60f22fbdd9381620cd5b6c04;hb=84b38ac86f1f92b91ae8913cd0dbcb5c3485dc3a;hp=dbbf0da0f4a17b225df93321cc8ffaf6230036a1;hpb=085cf66f8385f8cbc269c38ca7c7572d09e4810e;p=helm.git

diff --git a/matita/components/ng_tactics/nInversion.ml b/matita/components/ng_tactics/nInversion.ml
index dbbf0da0f..f1da10cb7 100644
--- a/matita/components/ng_tactics/nInversion.ml
+++ b/matita/components/ng_tactics/nInversion.ml
@@ -71,7 +71,7 @@ let rec jmeqpatt = function
 let rec mk_arrows ~jmeq xs ys selection target = 
   match selection,xs,ys with
     [],[],[] -> target
-  | false :: l,x::xs,y::ys -> mk_arrows ~jmeq xs ys l target
+  | false :: l,_x::xs,_y::ys -> mk_arrows ~jmeq xs ys l target
   | true :: l,x::xs,y::ys when jmeq ->
      NotationPt.Binder (`Forall, (mk_id "_",
        Some (mk_appl [mk_sym "jmsimeq" ; 
@@ -95,7 +95,7 @@ let subst_metasenv_and_fix_names status =
    status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv status subst metasenv,subst,o)
 ;;
 
-let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.status) baseuri =
+let mk_inverter ~jmeq name _is_ind it leftno ?selection outsort (status: #NCic.status) baseuri =
  pp (lazy ("leftno = " ^ string_of_int leftno));
  let _,ind_name,ty,cl = it in
  pp (lazy ("arity: " ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] ty));
@@ -110,11 +110,10 @@ let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.st
  let nparams = List.length args in
 
  (* the default is a dependent inversion *)
- (*let is_dependent = selection = None in*)
- let is_dependent = true in
+ let is_dependent = (selection = None && (jmeq || nparams = 0)) in
 
  pp (lazy ("nparams = " ^ string_of_int nparams));
- if nparams = 0 
+ if (nparams = 0 && not is_dependent)
    then raise (Failure "inverter: the type must have at least one right parameter") 
    else 
      let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (leftno+nparams+1)) in
@@ -143,7 +142,7 @@ let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.st
        in (hypaux 1 ncons)
      in
     
-     let outsort, suffix = NCicElim.ast_of_sort outsort in
+     let outsort, _suffix = NCicElim.ast_of_sort outsort in
      let theorem =
       mk_prods xs
        (NotationPt.Binder (`Forall, (mk_id "Hterm", Some (mk_appl (List.map mk_id (ind_name::xs)))),
@@ -151,13 +150,13 @@ let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.st
         mk_prods hyplist (mk_appl (mk_id "P"::id_rs))))))
      in
      let status, theorem =
-      GrafiteDisambiguate.disambiguate_nobj status ~baseuri 
+      let attrs = `Generated, `Theorem, `InversionPrinciple in 
+      GrafiteDisambiguate.disambiguate_nobj status ~baseuri
        (baseuri ^ name ^ ".def",0,
          NotationPt.Theorem
-          (`Theorem,name,theorem,
-            Some (NotationPt.Implicit (`Tagged "inv")),`InversionPrinciple))
+          (name,theorem, Some (NotationPt.Implicit (`Tagged "inv")), attrs))
      in 
-     let uri,height,nmenv,nsubst,nobj = theorem in
+     let _uri,_height,nmenv,_nsubst,_nobj = theorem in
      let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
      let status = status#set_obj theorem in
      let status = status#set_stack ninitial_stack in
@@ -176,7 +175,11 @@ NotationPt.Implicit (`Tagged "end"));
       "",0,(None,[],
         Some (if jmeq then jmeqpatt selection
                      else leibpatt selection)) in
-     let elim_tac = if is_ind then NTactics.elim_tac else NTactics.cases_tac in
+     (* let elim_tac = if is_ind then NTactics.elim_tac else NTactics.cases_tac in *)
+     let elim_tac ~what ~where s =
+       try NTactics.elim_tac ~what ~where s 
+       with NTacStatus.Error _ -> NTactics.cases_tac ~what ~where s
+     in
      let status =
       NTactics.block_tac 
        (NTactics.branch_tac ::
@@ -202,6 +205,6 @@ NotationPt.Implicit (`Tagged "end"));
 
 let mk_inverter name is_ind it leftno ?selection outsort status baseuri =
  try mk_inverter ~jmeq:true name is_ind it leftno ?selection outsort status baseuri
- with NTacStatus.Error (s,_) -> 
+ with NTacStatus.Error (_s,_) -> 
    mk_inverter ~jmeq:false name is_ind it leftno ?selection outsort status baseuri
 ;;