From cbe17d1d7b5116edfaf3fedd74fe4636f08f0c70 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 4 Apr 2008 09:57:41 +0000
Subject: Protection de rewrite in contre le dépliage des constantes dans
 w_unify, ce qui n'était pas encore fait

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10750 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/clenv.ml  | 4 ++--
 pretyping/clenv.mli | 2 +-
 2 files changed, 3 insertions(+), 3 deletions(-)

(limited to 'pretyping')

diff --git a/pretyping/clenv.ml b/pretyping/clenv.ml
index 0d462f793d..242368ce99 100644
--- a/pretyping/clenv.ml
+++ b/pretyping/clenv.ml
@@ -304,7 +304,7 @@ let connect_clenv gls clenv =
 
    In particular, it assumes that [env'] and [sigma'] extend [env] and [sigma].
 *)
-let clenv_fchain ?(allow_K=true) mv clenv nextclenv =
+let clenv_fchain ?(allow_K=true) ?(flags=default_unify_flags) mv clenv nextclenv =
   (* Add the metavars of [nextclenv] to [clenv], with their name-environment *)
   let clenv' =
     { templval = clenv.templval;
@@ -314,7 +314,7 @@ let clenv_fchain ?(allow_K=true) mv clenv nextclenv =
       env = nextclenv.env } in
   (* unify the type of the template of [nextclenv] with the type of [mv] *)
   let clenv'' =
-    clenv_unify allow_K CUMUL
+    clenv_unify allow_K ~flags:flags CUMUL
       (clenv_term clenv' nextclenv.templtyp)
       (clenv_meta_type clenv' mv)
       clenv' in
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 6a7038a078..4f27ec902f 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -61,7 +61,7 @@ val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> claus
 
 val connect_clenv : evar_info sigma -> clausenv -> clausenv
 val clenv_fchain : 
-  ?allow_K:bool -> metavariable -> clausenv -> clausenv -> clausenv
+  ?allow_K:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
 
 (***************************************************************)
 (* Unification with clenvs *)
-- 
cgit v1.2.3