diff options
| author | Pierre-Marie Pédrot | 2020-09-07 13:36:53 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2020-09-07 13:38:15 +0200 |
| commit | cd9ca8a10e79ed07836a0c212524bc5a3553e2ea (patch) | |
| tree | 824c612b941c986adc12d4ab4c4e4f2c2794b55b /proofs/clenv.mli | |
| parent | 48f465dd5c5f9db416a7cd57b0acb86f17323ce3 (diff) | |
Remove dead code in clenv-generating functions.
The *_env functions used to be different, but now they were just redundant
with their direct equivalent.
Diffstat (limited to 'proofs/clenv.mli')
| -rw-r--r-- | proofs/clenv.mli | 7 |
1 files changed, 0 insertions, 7 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli index d4905de434..a72c8c5e1f 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -75,17 +75,10 @@ val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv (** the arity of the lemma is fixed the optional int tells how many prods of the lemma have to be used use all of them if None *) -val make_clenv_binding_env_apply : - env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings -> - clausenv - val make_clenv_binding_apply : env -> evar_map -> int option -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv -val make_clenv_binding_env : - env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv - val make_clenv_binding : env -> evar_map -> EConstr.constr * EConstr.constr -> constr bindings -> clausenv |