let module C = Cic in
let module R = CicReduction in
let module P = PrimitiveTactics in
let module T = Tacticals in
let module S = ProofEngineStructuralRules in
let _,metasenv,_,_ = proof in
let module C = Cic in
let module R = CicReduction in
let module P = PrimitiveTactics in
let module T = Tacticals in
let module S = ProofEngineStructuralRules in
let _,metasenv,_,_ = proof in