let module C = Cic in
let module Con = Content in
let rec extend_premise_env current_env =
- function
+ function
[] -> current_env
- | p::atl ->
+ | p::atl ->
extend_premise_env
((p.Con.proof_id,(proof2cic current_env p))::current_env) atl in
let new_premise_env = extend_premise_env premise_env p.Con.proof_apply_context in