X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_tactics%2FnInversion.ml;h=8267fd87774e00398ea654d17ba0a6ff4111c1ae;hb=f9abd21eb0d26cf9b632af4df819225be4d091e3;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..8267fd877 100644
--- a/matita/components/ng_tactics/nInversion.ml
+++ b/matita/components/ng_tactics/nInversion.ml
@@ -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
@@ -151,11 +150,11 @@ 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 ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv 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 ::