diff options
| author | Chantal Keller <Chantal.Keller@inria.fr> | 2019-03-12 09:52:17 +0100 |
|---|---|---|
| committer | Chantal Keller <Chantal.Keller@inria.fr> | 2019-03-12 09:52:17 +0100 |
| commit | 4a610de645ca2bb505c97dd082220a57595019ad (patch) | |
| tree | 66775f6efb1a0a0980a399cff1d3d2bff31f14f7 /src/versions/native/structures.mli | |
| parent | e3ab22e6278670fadd5465327c5541d15049f526 (diff) | |
| download | smtcoq-4a610de645ca2bb505c97dd082220a57595019ad.tar.gz smtcoq-4a610de645ca2bb505c97dd082220a57595019ad.zip | |
Support for native-coq
Diffstat (limited to 'src/versions/native/structures.mli')
| -rw-r--r-- | src/versions/native/structures.mli | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/src/versions/native/structures.mli b/src/versions/native/structures.mli index abedc17..cae581e 100644 --- a/src/versions/native/structures.mli +++ b/src/versions/native/structures.mli @@ -11,7 +11,7 @@ (* Constr generation and manipulation *) -type id +type id = Names.variable val mkId : string -> id type name @@ -24,26 +24,26 @@ type types = constr val eq_constr : constr -> constr -> bool val hash_constr : constr -> int val mkProp : types -val mkConst : Names.Constant.t -> constr +val mkConst : Names.constant -> constr val mkVar : id -> constr val mkRel : int -> constr val isRel : constr -> bool val destRel : constr -> int val lift : int -> constr -> constr -val mkApp : constr -> constr array -> constr +val mkApp : constr * constr array -> constr val decompose_app : constr -> constr * constr list val mkLambda : name * types * constr -> constr val mkProd : name * types * types -> types val mkLetIn : name * constr * types * constr -> constr -val pr_constr_env : Environ.env -> constr -> Pp.t -val pr_constr : constr -> Pp.t +val pr_constr_env : Environ.env -> constr -> Pp.std_ppcmds +val pr_constr : constr -> Pp.std_ppcmds val mkUConst : constr -> Entries.definition_entry val mkTConst : constr -> 'a -> types -> Entries.definition_entry val declare_new_type : id -> types val declare_new_variable : id -> types -> constr -val declare_constant : id -> Safe_typing.private_constants Entries.definition_entry -> Names.Constant.t +val declare_constant : id -> Entries.definition_entry -> Names.constant type cast_kind val vmcast : cast_kind |