From f5bbb5ce34bb1ee2165086b0fdb3ee5f3d96a44e Mon Sep 17 00:00:00 2001
From: msozeau
Date: Fri, 19 Jul 2013 14:50:48 +0000
Subject: - Fix uncaught exception NotASort from reductionops, moving
 decomp_sort to retyping.ml - In unification's w_merge, assign the evars in
 the same order they were found. Might create rare incompatibilities.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16632 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/reductionops.ml | 12 +++---------
 1 file changed, 3 insertions(+), 9 deletions(-)

(limited to 'pretyping/reductionops.ml')

diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index b2a9bdcc55..e86732658b 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -939,16 +939,10 @@ let splay_lam_n env sigma n =
   in
   decrec env n empty_rel_context
 
-exception NotASort
-
-let decomp_sort env sigma t =
+let is_sort env sigma t =
   match kind_of_term (whd_betadeltaiota env sigma t) with
-  | Sort s -> s
-  | _ -> raise NotASort
-
-let is_sort env sigma arity =
-  try let _ = decomp_sort env sigma arity in true
-  with NotASort -> false
+  | Sort s -> true
+  | _ -> false
 
 (* reduction to head-normal-form allowing delta/zeta only in argument
    of case/fix (heuristic used by evar_conv) *)
-- 
cgit v1.2.3