diff options
| author | Matthieu Sozeau | 2017-05-29 18:54:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau | 2017-05-29 18:54:46 +0200 |
| commit | 563d173d86cb8fbaccad70ee4c665aa60beb069c (patch) | |
| tree | 4b23de3d24fd3d4d5bf9b8dbae7664a970931764 /vernac/indschemes.mli | |
| parent | ef8cf82668a794f116ae714749f434e3505880d1 (diff) | |
Pretyping cleanup: remove constr_of_global calls
Diffstat (limited to 'vernac/indschemes.mli')
| -rw-r--r-- | vernac/indschemes.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/vernac/indschemes.mli b/vernac/indschemes.mli index e5d79fd514..0f559d2bd8 100644 --- a/vernac/indschemes.mli +++ b/vernac/indschemes.mli @@ -40,7 +40,7 @@ val do_scheme : (Id.t located option * scheme) list -> unit (** Combine a list of schemes into a conjunction of them *) -val build_combined_scheme : env -> constant list -> constr * types +val build_combined_scheme : env -> constant list -> Evd.evar_map * constr * types val do_combined_scheme : Id.t located -> Id.t located list -> unit |