aboutsummaryrefslogtreecommitdiffhomepage
path: root/contrib/interface/translate.mli
blob: 41c33d5a3efd26a899a126bab92fd4674a6b27d3 (plain)
1
2
3
4
5
6
7
8
open Ascent;;
open Evd;;
open Proof_type;;
open Environ;;
open Term;;

val translate_goal : goal -> ct_RULE;;
val translate_constr : env -> constr -> ct_FORMULA;;