From 8cf4e04fa817cf7ff9d73cb5cb7fff8b3b950387 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 18 Oct 2008 15:57:24 +0000
Subject: Optimisation de clenv.ml pour que meta_instance ne soit pas appelé
 abusivement sur les clauses. Nettoyage au passage de metamap qui était
 utilisé à la fois pour les substitutions de meta et pour les contextes de
 typage de meta.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@11467 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 tactics/setoid_replace.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'tactics/setoid_replace.ml')

diff --git a/tactics/setoid_replace.ml b/tactics/setoid_replace.ml
index 644a68666a..22596ac3c0 100644
--- a/tactics/setoid_replace.ml
+++ b/tactics/setoid_replace.ml
@@ -1815,7 +1815,7 @@ let relation_rewrite c1 c2 (input_direction,cl) ~new_goals gl =
 let analyse_hypothesis gl c =
  let ctype = pf_type_of gl c in
  let eqclause  = Clenv.make_clenv_binding gl (c,ctype) Rawterm.NoBindings in
- let (equiv, args) = decompose_app (Clenv.clenv_type eqclause) in
+ let (equiv, args) = decompose_app (Clenv.clenv_direct_nf_type eqclause) in
  let rec split_last_two = function
    | [c1;c2] -> [],(c1, c2)
    | x::y::z ->
-- 
cgit v1.2.3