diff options
| author |  Matthieu Sozeau <mattam@mattam.org> | 2013-10-17 14:55:57 +0200 |
|---|---|---|
| committer | Matthieu Sozeau <mattam@mattam.org> | 2014-05-06 09:58:53 +0200 |
| commit | 84cbc09bd1400f732a6c70e8a840e4c13d018478 (patch) | |
| tree | f6b3417e653bea9de8f0d8f510ad19ccdbb4840e /pretyping/evd.mli | |
| parent | 57bee17f928fc67a599d2116edb42a59eeb21477 (diff) | |
Correct rebase on STM code. Thanks to E. Tassi for help on dealing with
latent universes. Now the universes in the type of a definition/lemma
are eagerly added to the environment so that later proofs can be checked
independently of the original (delegated) proof body.
- Fixed firstorder, ring to work correctly with universe polymorphism.
- Changed constr_of_global to raise an anomaly if side effects would be lost by
turning a polymorphic constant into a constr.
- Fix a non-termination issue in solve_evar_evar.
-
Diffstat (limited to 'pretyping/evd.mli')
| -rw-r--r-- | pretyping/evd.mli | 8 |
1 files changed, 6 insertions, 2 deletions
diff --git a/pretyping/evd.mli b/pretyping/evd.mli index 18d68bebf..e44e8e906 100644 --- a/pretyping/evd.mli +++ b/pretyping/evd.mli @@ -226,7 +226,8 @@ val instantiate_evar_array : evar_info -> constr -> constr array -> constr val subst_evar_defs_light : substitution -> evar_map -> evar_map (** Assume empty universe constraints in [evar_map] and [conv_pbs] *) -val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> evar_map -> evar_map -> evar_map +val evars_reset_evd : ?with_conv_pbs:bool -> ?with_univs:bool -> + evar_map -> evar_map -> evar_map (** spiwack: this function seems to somewhat break the abstraction. *) (** {6 Misc} *) @@ -283,12 +284,14 @@ type 'a sigma = { val sig_it : 'a sigma -> 'a val sig_sig : 'a sigma -> evar_map +val on_sig : 'a sigma -> (evar_map -> evar_map * 'b) -> 'a sigma * 'b (** {5 The state monad with state an evar map} *) module MonadR : Monad.S with type +'a t = evar_map -> evar_map * 'a module Monad : Monad.S with type +'a t = evar_map -> 'a * evar_map + (** {5 Meta machinery} These functions are almost deprecated. They were used before the @@ -478,7 +481,8 @@ val fresh_constant_instance : env -> evar_map -> constant -> evar_map * pconstan val fresh_inductive_instance : env -> evar_map -> inductive -> evar_map * pinductive val fresh_constructor_instance : env -> evar_map -> constructor -> evar_map * pconstructor -val fresh_global : ?rigid:rigid -> env -> evar_map -> Globnames.global_reference -> evar_map * constr +val fresh_global : ?rigid:rigid -> env -> evar_map -> + Globnames.global_reference -> evar_map * constr (******************************************************************** Conversion w.r.t. an evar map: might generate universe unifications |