- (** create a Cic.CurrentProof from a given proof *)
-let currentProof (uri, metasenv, bo, ty) =
- let uri = MatitaTypes.unopt_uri uri in
- (* TODO CSC: Wrong: [] is just plainly wrong *)
- Cic.CurrentProof (UriManager.name_of_uri uri, metasenv, bo, ty, [])