let module C = Cic in
let module U = UriManager in
let curi,metasenv,pbo,pty = proof in
- let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,gty = CicUtil.lookup_meta goal metasenv in
let eq_ind_r,ty,t1,t2 =
match CicTypeChecker.type_of_aux' metasenv context equality with
C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
let module C = Cic in
let module U = UriManager in
let curi,metasenv,pbo,pty = proof in
- let metano,context,gty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,gty = CicUtil.lookup_meta goal metasenv in
let eq_ind_r,ty,t1,t2 =
match CicTypeChecker.type_of_aux' metasenv context equality with
C.Appl [C.MutInd (uri,0,[]) ; ty ; t1 ; t2]
let module P = PrimitiveTactics in
let module T = Tacticals in
let _,metasenv,_,_ = proof in
- let _,context,_ = List.find (function (m,_,_) -> m=goal) metasenv in
+ let _,context,_ = CicUtil.lookup_meta goal metasenv in
let wty = CicTypeChecker.type_of_aux' metasenv context what in
try
if (wty = (CicTypeChecker.type_of_aux' metasenv context with_what))
let module R = CicReduction in
let module U = UriManager in
let (_,metasenv,_,_) = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
match (R.whd context ty) with
(C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (U.eq uri (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
PrimitiveTactics.apply_tac ~status:(proof,goal)
let module U = UriManager in
let module T = Tacticals in
let (_,metasenv,_,_) = proof in
- let metano,context,ty = List.find (function (m,_,_) -> m=goal) metasenv in
+ let metano,context,ty = CicUtil.lookup_meta goal metasenv in
match (R.whd context ty) with
(C.Appl [(C.MutInd (uri, 0, [])); _; _; _]) when (uri = (U.uri_of_string "cic:/Coq/Init/Logic/eq.ind")) ->
T.thens