diff options
| author | Emilio Jesus Gallego Arias | 2019-07-04 10:27:35 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-07-04 10:27:35 +0200 |
| commit | 1c9aa339042030f756d1957abed7d3b698ff83f5 (patch) | |
| tree | ea8da28bdd5b230974cdf3c3fa35fbd9d411963d /kernel | |
| parent | a661aadbc7120b93ccf8507c0173ffd6cfa3a0f8 (diff) | |
| parent | 1cc661d18f67f71a494b525b1f82fd9133ee5a3c (diff) | |
Merge PR #10461: Simplify Declare.declare_variable
Reviewed-by: ejgallego
Reviewed-by: maximedenes
Reviewed-by: ppedrot
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/safe_typing.ml | 11 | ||||
| -rw-r--r-- | kernel/safe_typing.mli | 4 |
2 files changed, 6 insertions, 9 deletions
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml index 445e359dee..24b3765019 100644 --- a/kernel/safe_typing.ml +++ b/kernel/safe_typing.ml @@ -428,12 +428,11 @@ let push_named_def (id,de) senv = let env'' = safe_push_named (LocalDef (x, c, typ)) senv.env in { senv with env = env'' } -let push_named_assum ((id,t,poly),ctx) senv = - let senv' = push_context_set poly ctx senv in - let t, r = Term_typing.translate_local_assum senv'.env t in - let x = Context.make_annot id r in - let env'' = safe_push_named (LocalAssum (x,t)) senv'.env in - {senv' with env=env''} +let push_named_assum (x,t) senv = + let t, r = Term_typing.translate_local_assum senv.env t in + let x = Context.make_annot x r in + let env'' = safe_push_named (LocalAssum (x,t)) senv.env in + {senv with env=env''} (** {6 Insertion of new declarations to current environment } *) diff --git a/kernel/safe_typing.mli b/kernel/safe_typing.mli index 50f6832ffa..c3d0965857 100644 --- a/kernel/safe_typing.mli +++ b/kernel/safe_typing.mli @@ -69,9 +69,7 @@ val is_joined_environment : safe_environment -> bool (** Insertion of local declarations (Local or Variables) *) -val push_named_assum : - (Id.t * Constr.types * bool (* polymorphic *)) - Univ.in_universe_context_set -> safe_transformer0 +val push_named_assum : (Id.t * Constr.types) -> safe_transformer0 (** Returns the full universe context necessary to typecheck the definition (futures are forced) *) |