diff options
Diffstat (limited to 'src/trace/coqInterface.mli')
| -rw-r--r-- | src/trace/coqInterface.mli | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/src/trace/coqInterface.mli b/src/trace/coqInterface.mli index 453bce1..f4fff30 100644 --- a/src/trace/coqInterface.mli +++ b/src/trace/coqInterface.mli @@ -100,10 +100,9 @@ type constr_expr = Constrexpr.constr_expr val error : string -> 'a val anomaly : string -> 'a val warning : string -> string -> unit -val extern_constr : constr -> constr_expr val destruct_rel_decl : (constr, types) Context.Rel.Declaration.pt -> name * types val interp_constr : Environ.env -> Evd.evar_map -> constr_expr -> constr -val ppconstr_lsimpleconstr : Notation_gram.tolerability +val ppconstr_lsimpleconstr : Constrexpr.entry_relative_level val constrextern_extern_constr : constr -> constr_expr val get_rel_dec_name : (constr, types) Context.Rel.Declaration.pt -> name val retyping_get_type_of : Environ.env -> Evd.evar_map -> constr -> constr |