+ProofEngineTypes.mk_tactic (private_inversion_tac ~term)
+;;
+
+
+let inversion_tac ~term =
+ let module T = CicTypeChecker in
+ let module R = CicReduction in
+ let module C = Cic in
+ let module P = PrimitiveTactics in
+ let module PET = ProofEngineTypes in
+ let inversion_tac ~term (proof, goal) =
+ (*DEBUG*) debug_print (lazy ("inversion begins"));
+ let _,metasenv,_subst,_,_, _ = proof in
+ let (_,context,goalty) = CicUtil.lookup_meta goal metasenv in
+ let termty,_ = T.type_of_aux' metasenv context term CicUniv.oblivion_ugraph in
+ let uri, typeno =
+ match termty with
+ | Cic.MutInd (uri,typeno,_)
+ | Cic.Appl(Cic.MutInd (uri,typeno,_)::_) -> uri,typeno
+ | _ -> assert false
+ in
+ (* let uri = baseuri_of_term termty in *)
+ let obj,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
+ let name,nleft,arity,cons_list =
+ match obj with
+ Cic.InductiveDefinition (tys,_,nleft,_) ->
+ let (name,_,arity,cons_list) = List.nth tys typeno in
+ (name,nleft,arity,cons_list)
+ |_ -> assert false
+ in
+ let buri = UriManager.buri_of_uri uri in
+ let inversor_uri =
+ UriManager.uri_of_string (buri ^ "/" ^ name ^ "_inv" ^ ".con") in
+ (* arity length = number of parameters plus 1 *)
+ let arity_length = (List.length (term_to_list termty)) in
+ (* Check the existence of any right parameter. *)
+ assert (arity_length > (nleft + 1));
+ let appl_term arity_consno uri =
+ let l = [] in
+ let a = ref l in
+ for n = 1 to arity_consno do
+ a := (Cic.Implicit None)::(!a)
+ done;
+ (* apply i_inv ? ...? H). *)
+ Cic.Appl ([Cic.Const(uri,[])] @ !a @ [term])
+ in
+ let t = appl_term (arity_length + (List.length cons_list)) inversor_uri in
+ let (t1,metasenv,_subst,t3,t4, attrs) = proof in
+ let (ref_t,_,metasenv'',_) = CicRefine.type_of_aux' metasenv context t
+ CicUniv.oblivion_ugraph
+ in
+ let proof = (t1,metasenv'',_subst,t3,t4, attrs) in
+ let proof3,gl3 =
+ ProofEngineTypes.apply_tactic (P.apply_tac ref_t) (proof,goal) in
+ let patched_new_goals =
+ let (_,metasenv''',_subst,_,_, _) = proof3 in
+ let new_goals = ProofEngineHelpers.compare_metasenvs
+ ~oldmetasenv:metasenv ~newmetasenv:metasenv''
+ in
+ List.filter (function i -> List.exists (function (j,_,_) -> j=i)
+ metasenv''') new_goals @ gl3
+ in
+ (proof3, patched_new_goals)
+ in