From 08e2c28ee98c6a5d235cc9b84bc5690dd9a22666 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 1 Jun 2000 20:51:48 +0000
Subject: Mise en place d'un choix constr/typed_type en remplacement de
 certains Cast

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

(limited to 'proofs')

diff --git a/proofs/tacinterp.ml b/proofs/tacinterp.ml
index bd7ff32a76..6d999b9c5d 100644
--- a/proofs/tacinterp.ml
+++ b/proofs/tacinterp.ml
@@ -588,7 +588,7 @@ and cvt_pattern (evc,env,lfun,lmatch,goalopt)=function
       in
         let jdt=Typing.unsafe_machine env evc csr
         in
-          (occs, jdt.Environ.uj_val, jdt.Environ.uj_type)
+          (occs, jdt.Environ.uj_val, body_of_type jdt.Environ.uj_type)
   |arg -> invalid_arg_loc (Ast.loc arg,"cvt_pattern")
 and cvt_unfold (evc,env,lfun,lmatch,goalopt)=function
    Node(_,"UNFOLD", com::nums) ->
-- 
cgit v1.2.3