X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fng_tactics%2FnTactics.ml;h=67568154088e1d54f47c7b6de7662044166354ce;hb=ef6a409b9cea2a3d0b0852ae3e69737566c91ba1;hp=f5ae3a721e4880a955d4be5463252cf4423e2a36;hpb=12f96bd48b460d06f9858a334ee7c52d6831712f;p=helm.git

diff --git a/helm/software/components/ng_tactics/nTactics.ml b/helm/software/components/ng_tactics/nTactics.ml
index f5ae3a721..675681540 100644
--- a/helm/software/components/ng_tactics/nTactics.ml
+++ b/helm/software/components/ng_tactics/nTactics.ml
@@ -652,3 +652,26 @@ let assert_tac seqs status =
      ) status
 ;;
 
+let inversion_tac ~what:(txt,len,what) ~where = 
+  let what = txt, len, Ast.Appl [what; Ast.Implicit `Vector] in
+  let indtyinfo = ref None in
+  let sort = ref (NCic.Rel 1) in
+  atomic_tac (block_tac [
+    analyze_indty_tac ~what indtyinfo;    
+    (fun s -> select_tac 
+      ~where ~job:(`Substexpand ((HExtlib.unopt !indtyinfo).rightno+1)) true s);
+    sort_of_goal_tac sort;
+    (fun status ->
+     let ity = HExtlib.unopt !indtyinfo in
+     let NReference.Ref (uri, _) = ity.reference in
+     let name = 
+       NUri.name_of_uri uri ^ "_inv_" ^
+        snd (NCicElim.ast_of_sort 
+          (match !sort with NCic.Sort x -> x | _ -> assert false))
+     in
+     let eliminator = 
+       let _,_,w = what in
+       Ast.Appl [ Ast.Ident (name,None) ; Ast.Implicit `Vector ; w ]
+     in
+     exact_tac ("",0,eliminator) status) ]) 
+;;