From 540a93a8e6665f70b2a61158728d6b85be101274 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sun, 17 Oct 2004 08:47:12 +0000
Subject: Vérification de la typability de 'pattern'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@6226 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/tacred.ml | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 88928d97f5..a48881bd74 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -795,18 +795,18 @@ let compute = cbv_betadeltaiota
 (* gives [na:ta]c' such that c converts to ([na:ta]c' a), abstracting only
  * the specified occurrences. *)
 
-let abstract_scheme env sigma (locc,a) t =
+let abstract_scheme env sigma (locc,a) c =
   let ta = Retyping.get_type_of env sigma a in
   let na = named_hd env ta Anonymous in
   if occur_meta ta then error "cannot find a type for the generalisation";
   if occur_meta a then 
-    mkLambda (na,ta,t)
+    mkLambda (na,ta,c)
   else 
-    mkLambda (na, ta,subst_term_occ locc a t)
-
+    mkLambda (na,ta,subst_term_occ locc a c)
 
 let pattern_occs loccs_trm env sigma c =
   let abstr_trm = List.fold_right (abstract_scheme env sigma) loccs_trm c in
+  let _ = Typing.type_of env sigma abstr_trm in
   applist(abstr_trm, List.map snd loccs_trm)
 
 (* Generic reduction: reduction functions used in reduction tactics *)
-- 
cgit v1.2.3