+
+ and ce2pres_in_joint_context_element = function
+ | `Inductive _ -> assert false (* TODO *)
+ | (`Declaration _) as x -> ce2pres x
+ | (`Hypothesis _) as x -> ce2pres x
+ | (`Proof _) as x -> ce2pres x
+ | (`Definition _) as x -> ce2pres x
+
+ and ce2pres_in_proof_context_element = function
+ | `Joint ho ->
+ B.H ([],(List.map ce2pres_in_joint_context_element ho.Content.joint_defs))
+ | (`Declaration _) as x -> ce2pres x
+ | (`Hypothesis _) as x -> ce2pres x
+ | (`Proof _) as x -> ce2pres x
+ | (`Definition _) as x -> ce2pres x
+
+ and ce2pres =