diff options
| -rw-r--r-- | proofs/clenv.ml | 6 | ||||
| -rw-r--r-- | proofs/clenv.mli | 7 |
2 files changed, 0 insertions, 13 deletions
diff --git a/proofs/clenv.ml b/proofs/clenv.ml index 4893758ab3..31bc698830 100644 --- a/proofs/clenv.ml +++ b/proofs/clenv.ml @@ -713,12 +713,6 @@ let make_clenv_binding_gen hyps_only n env sigma (c,t) = function | NoBindings -> mk_clenv_from_env env sigma n (c,t) -let make_clenv_binding_env_apply env sigma n = - make_clenv_binding_gen true n env sigma - -let make_clenv_binding_env env sigma = - make_clenv_binding_gen false None env sigma - let make_clenv_binding_apply env sigma n = make_clenv_binding_gen true n env sigma let make_clenv_binding env sigma = make_clenv_binding_gen false None env sigma 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 |