diff options
| author | Pierre-Marie Pédrot | 2017-07-21 14:49:16 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-08-01 16:11:55 +0200 |
| commit | cabce8ae233040c2365bfd8bd1f478676fcade33 (patch) | |
| tree | 92bd7153a50e16ed98ceda7a70489df7f8a97ba3 /API | |
| parent | 65bd1deac80689d02be7ef580872974cc38bf93c (diff) | |
Detyping functions are now operating on EConstr.t.
This was already the case, but the API was not exposing this.
Diffstat (limited to 'API')
| -rw-r--r-- | API/API.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/API/API.mli b/API/API.mli index a0e77edd12..f3ed7a894f 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4283,10 +4283,10 @@ module Constrextern : sig val extern_glob_constr : Names.Id.Set.t -> Glob_term.glob_constr -> Constrexpr.constr_expr val extern_glob_type : Names.Id.Set.t -> Glob_term.glob_constr -> Constrexpr.constr_expr - val extern_constr : ?lax:bool -> bool -> Environ.env -> Evd.evar_map -> Constr.t -> Constrexpr.constr_expr + val extern_constr : ?lax:bool -> bool -> Environ.env -> Evd.evar_map -> EConstr.t -> Constrexpr.constr_expr val without_symbols : ('a -> 'b) -> 'a -> 'b val print_universes : bool ref - val extern_type : bool -> Environ.env -> Evd.evar_map -> Term.types -> Constrexpr.constr_expr + val extern_type : bool -> Environ.env -> Evd.evar_map -> EConstr.t -> Constrexpr.constr_expr val with_universes : ('a -> 'b) -> 'a -> 'b val set_extern_reference : (?loc:Loc.t -> Names.Id.Set.t -> Globnames.global_reference -> Libnames.reference) -> unit |