blob: 0f3113bf60eca7c9946465daf74b2b02b2b3f603 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
|
(* $Id$ *)
(*i*)
open Names
open Term
open Environ
(*i*)
val dbize_op :
Coqast.loc -> string -> Coqast.t list -> pseudo_constr list -> pseudo_constr
val dbize : unit assumptions -> Coqast.t -> pseudo_constr
val absolutize_cci : unsafe_env -> pseudo_constr -> pseudo_constr
val dbize_cci : unsafe_env -> Coqast.t -> pseudo_constr
val absolutize_fw : unsafe_env -> pseudo_constr -> pseudo_constr
val dbize_fw : unsafe_env -> Coqast.t -> pseudo_constr
val raw_pseudo_constr_of_com : unsafe_env -> Coqast.t -> pseudo_constr
val raw_fpseudo_constr_of_com : unsafe_env -> Coqast.t -> pseudo_constr
val raw_pseudo_constr_of_compattern : unsafe_env -> Coqast.t -> pseudo_constr
val globalize_command : Coqast.t -> Coqast.t
val globalize_ast : Coqast.t -> Coqast.t
|
