diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-09 18:23:23 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2010-06-09 18:23:23 +0000 |
| commit | 43fede22d500a7234a82aaae77adfebff8006c4f (patch) | |
| tree | bedcaff6b1ad79330f39f33b38cce4c0208bb733 /proofs/clenv.mli | |
| parent | 2cf5036431304d5a3e6393d5fd5827798ea98983 (diff) | |
Fix bug #2317: setoid_rewrite ignored binding lists. Slightly
generalize the interface of Clenv to be able to use the existing
treatment of bindings. Clenv functions did not use goals conclusions
but insisted on getting goals anyway (which is even more problematic as
goals appear in evar maps now).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13102 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'proofs/clenv.mli')
| -rw-r--r-- | proofs/clenv.mli | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/proofs/clenv.mli b/proofs/clenv.mli index afda6d931..209024c9c 100644 --- a/proofs/clenv.mli +++ b/proofs/clenv.mli @@ -97,6 +97,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 -> constr * constr -> constr bindings -> + clausenv + val make_clenv_binding_apply : Goal.goal sigma -> int option -> constr * constr -> constr bindings -> clausenv |