diff options
| author | Gaëtan Gilbert | 2020-02-06 17:41:49 +0100 |
|---|---|---|
| committer | Gaëtan Gilbert | 2020-02-06 21:17:56 +0100 |
| commit | 48b142d0e915e946274c14ab354f174cc5b6df51 (patch) | |
| tree | dbae5f5dc02cacfa39f11553ff537889eb818299 /proofs | |
| parent | 6bf68189b74fed332a064257b9f1b7e46b6309b5 (diff) | |
Remove Clenv.mk_clenv_type_of (hidden unsafe_type_of)
Diffstat (limited to 'proofs')
| -rw-r--r-- | proofs/clenv.ml | 6 | ||||
| -rw-r--r-- | proofs/clenv.mli | 1 |
2 files changed, 0 insertions, 7 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index bb660adf4d..b0eb8dc646 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -128,12 +128,6 @@ let mk_clenv_from_n gls n (c,cty) = let mk_clenv_from gls = mk_clenv_from_n gls None -let mk_clenv_type_of gls t = - let env = Proofview.Goal.env gls in - let sigma = Tacmach.New.project gls in - let sigma, tt = Typing.type_of env sigma t in - mk_clenv_from_env env sigma None (t,tt) - (******************************************************************) (* [mentions clenv mv0 mv1] is true if mv1 is defined and mentions diff --git a/proofs/clenv.mli b/proofs/clenv.mli index 3fca967395..7213c9318c 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -46,7 +46,6 @@ val clenv_meta_type : clausenv -> metavariable -> types val mk_clenv_from : Proofview.Goal.t -> EConstr.constr * EConstr.types -> clausenv val mk_clenv_from_n : Proofview.Goal.t -> int option -> EConstr.constr * EConstr.types -> clausenv -val mk_clenv_type_of : Proofview.Goal.t -> EConstr.constr -> clausenv val mk_clenv_from_env : env -> evar_map -> int option -> EConstr.constr * EConstr.types -> clausenv (** Refresh the universes in a clenv *) |