From b7fcbb07f8b484707a86eb06df1bd7116fb55a21 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 5 Oct 2011 14:34:17 +0000
Subject: It happens that the type inference algorithm (pretyping) did not
 check that the return predicate of the match construction is at an allowed
 sort, resulting in tactics possibly manipulating ill-typed terms. This is now
 fixed,

Incidentally removed in pretyping an ill-placed coercion.

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

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 834c27969e..e8acd67caf 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -770,7 +770,7 @@ let splay_arity env sigma c =
     | Sort s -> l,s
     | _ -> invalid_arg "splay_arity"
 
-let sort_of_arity env c = snd (splay_arity env Evd.empty c)
+let sort_of_arity env sigma c = snd (splay_arity env sigma c)
 
 let splay_prod_n env sigma n =
   let rec decrec env m ln c = if m = 0 then (ln,c) else
-- 
cgit v1.2.3