diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-08-16 09:44:28 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-08-16 09:44:28 +0200 |
| commit | e1264c9f0d50bf8ca09fa7388101daa0b4c29635 (patch) | |
| tree | 3358d182b655bb2510c1d99872ac733474c9124a /API/API.mli | |
| parent | 09b54382e52b572f8c091993309adcc4fea3a093 (diff) | |
| parent | cf906af70f5c48cab99bd89047af0b2831850cf1 (diff) | |
Merge PR #912: Detyping functions are now operating on EConstr.t.
Diffstat (limited to 'API/API.mli')
| -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 a99cd2a9a..5804a82f6 100644 --- a/API/API.mli +++ b/API/API.mli @@ -4289,10 +4289,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 |