From f9d7ccaf40f7f21ce0630c9b668581249a635de9 Mon Sep 17 00:00:00 2001 From: herbelin Date: Fri, 12 Oct 2007 13:36:02 +0000 Subject: Uniformisation du comportement de rewrite et rewrite in : quand le filtrage d'ordre 2 échoue à trouver un prédicat de réécriture qui n'est pas une K-abstraction, les deux rewrite essaie alors le filtrage d'ordre 1. Ce n'est pas le plus élégant mais c'est la solution uniforme permettant d'être conservatif. MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10221 85f007b7-540e-0410-9357-904b9bb8a0f7 --- pretyping/clenv.mli | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'pretyping/clenv.mli') diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli index 73a171b8d..8546a44ef 100644 --- a/pretyping/clenv.mli +++ b/pretyping/clenv.mli @@ -61,7 +61,8 @@ val mk_clenv_type_of : evar_info sigma -> constr -> clausenv (* linking of clenvs *) val connect_clenv : evar_info sigma -> clausenv -> clausenv -val clenv_fchain : metavariable -> clausenv -> clausenv -> clausenv +val clenv_fchain : + ?allow_K:bool -> metavariable -> clausenv -> clausenv -> clausenv (***************************************************************) (* Unification with clenvs *) -- cgit v1.2.3