From 2f62592cd35492c816a4672c364721781d28102a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 18 May 2000 18:07:31 +0000
Subject: bug (typage avec meta)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@455 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 proofs/clenv.ml | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/proofs/clenv.ml b/proofs/clenv.ml
index 721552fad0..effc8d4697 100644
--- a/proofs/clenv.ml
+++ b/proofs/clenv.ml
@@ -547,8 +547,6 @@ let clenv_wtactic wt clenv =
     hook = wt clenv.hook }
 
 let clenv_type_of ce c =
-  Typing.type_of (w_env ce.hook) (w_Underlying ce.hook) c
-  (***
   let metamap =
     List.map 
       (function
@@ -556,6 +554,9 @@ let clenv_type_of ce c =
          | (n,Cltyp typ)    -> (n,typ.rebus))
       (intmap_to_list ce.env)
   in
+    Retyping.get_type_of_with_meta (w_env ce.hook) (w_Underlying ce.hook) metamap c
+(*  Typing.type_of (w_env ce.hook) (w_Underlying ce.hook) c *)
+  (***
   (Pretyping.ise_resolve true (w_Underlying ce.hook) metamap
      (gLOB(w_hyps ce.hook)) c).uj_type
   ***)
-- 
cgit v1.2.3