blob: 9f25ce38a4b25de70ce643036140ff3d9fb6ae8d (
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 pr_lconstr_env and ast_of_constr) *)
val translate_constr : bool -> env -> constr -> ct_FORMULA;;
val translate_path : int list -> ct_SIGNED_INT_LIST;;
|
