diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2017-05-29 18:54:46 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2017-05-29 18:54:46 +0200 |
| commit | 563d173d86cb8fbaccad70ee4c665aa60beb069c (patch) | |
| tree | 4b23de3d24fd3d4d5bf9b8dbae7664a970931764 /pretyping/program.mli | |
| parent | ef8cf82668a794f116ae714749f434e3505880d1 (diff) | |
Pretyping cleanup: remove constr_of_global calls
Diffstat (limited to 'pretyping/program.mli')
| -rw-r--r-- | pretyping/program.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/program.mli b/pretyping/program.mli index 94a7bdcb6..8439b9528 100644 --- a/pretyping/program.mli +++ b/pretyping/program.mli @@ -32,8 +32,8 @@ val coq_eq_rect : unit -> global_reference val coq_JMeq_ind : unit -> global_reference val coq_JMeq_refl : unit -> global_reference -val mk_coq_and : constr list -> constr -val mk_coq_not : constr -> constr +val mk_coq_and : Evd.evar_map -> constr list -> Evd.evar_map * constr +val mk_coq_not : Evd.evar_map -> constr -> Evd.evar_map * constr (** Polymorphic application of delayed references *) val papp : Evd.evar_map ref -> (unit -> global_reference) -> constr array -> constr |