-
-let elim_tac ~term ~status:(proof, goal) =
- let module T = CicTypeChecker in
- let module U = UriManager in
- let module R = CicReduction in
- let module C = Cic in
- let (curi,metasenv,_,_) = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
- let termty = T.type_of_aux' metasenv context term in
- let uri,exp_named_subst,typeno,args =
- match termty with
- C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
- | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
- (uri,exp_named_subst,typeno,args)
- | _ -> raise NotAnInductiveTypeToEliminate
- in
- let eliminator_uri =
- let buri = U.buri_of_uri uri in
- let name =
- match CicEnvironment.get_obj uri with
- C.InductiveDefinition (tys,_,_) ->
- let (name,_,_,_) = List.nth tys typeno in
- name
- | _ -> assert false
- in
- let ext =
- match T.type_of_aux' metasenv context ty with
- C.Sort C.Prop -> "_ind"
- | C.Sort C.Set -> "_rec"
- | C.Sort C.Type -> "_rect"
- | _ -> assert false
- in
- U.uri_of_string (buri ^ "/" ^ name ^ ext ^ ".con")
+let elim_tac ~term =
+ let elim_tac ~term (proof, goal) =
+ let module T = CicTypeChecker in
+ let module U = UriManager in
+ let module R = CicReduction in
+ let module C = Cic in
+ let (curi,metasenv,proofbo,proofty) = proof in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
+ let termty,_ = T.type_of_aux' metasenv context term CicUniv.empty_ugraph in
+ (* TASSI: FIXME *)
+ let uri,exp_named_subst,typeno,args =
+ match termty with
+ C.MutInd (uri,typeno,exp_named_subst) -> (uri,exp_named_subst,typeno,[])
+ | C.Appl ((C.MutInd (uri,typeno,exp_named_subst))::args) ->
+ (uri,exp_named_subst,typeno,args)
+ | _ -> raise NotAnInductiveTypeToEliminate