Stream: Coq users

Topic: How to access the function listed after Drop + use include

Vincent Siles (Sep 18 2020 at 09:52):

Hi ! Still on my journey with Drop.. After using #use "include";;, I see

val get_current_context : unit -> Evd.evar_map * Environ.env = <fun>

However if I enter get_current_context the type says

# get_current_context;;
- : Proof_global.t -> Evd.evar_map * Environ.env = <fun>

Are they the same function ? How can I get a Proof_global.t ? Sorry for the vague question but I've difficulties to navigate in the ocaml top level :)

Last updated: Oct 13 2024 at 01:02 UTC