blob: 65d8331b2d99a680650e05abc008d65be45c4529 (
plain)
1
2
3
4
5
6
7
8
9
10
11
|
open Ascent;;
open Evd;;
open Proof_type;;
open Environ;;
open Term;;
val translate_goal : goal -> ct_RULE;;
(* The boolean argument indicates whether names from the environment should *)
(* be avoided (same interpretation as for prterm_env and ast_of_constr) *)
val translate_constr : bool -> env -> constr -> ct_FORMULA;;
val translate_path : int list -> ct_SIGNED_INT_LIST;;
|
