- let rewrite_tac ~term:equality (proof,goal) =
- let module C = Cic in
- let module U = UriManager in
- let curi,metasenv,pbo,pty = proof in
- let metano,context,gty = CicUtil.lookup_meta goal metasenv in
+ let rewrite_tac ~term:equality (proof,goal) =
+ let module C = Cic in
+ let module U = UriManager in
+ let curi,metasenv,pbo,pty = proof in
+ let metano,context,gty = CicUtil.lookup_meta goal metasenv in
+ let ty_eq,_ =
+ CicTypeChecker.type_of_aux' metasenv context equality
+ CicUniv.empty_ugraph in