From 98f3621b5b0c50aaa48c86e1d6a4269d94388bd3 Mon Sep 17 00:00:00 2001
From: ppedrot
Date: Tue, 13 Nov 2012 22:38:16 +0000
Subject: More monomorphizations

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15969 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 interp/constrexpr_ops.ml | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

(limited to 'interp')

diff --git a/interp/constrexpr_ops.ml b/interp/constrexpr_ops.ml
index 306fbfad95..6b45c88975 100644
--- a/interp/constrexpr_ops.ml
+++ b/interp/constrexpr_ops.ml
@@ -73,9 +73,10 @@ let local_binder_loc = function
   | LocalRawDef ((loc,_),t) -> Loc.merge loc (constr_loc t)
   | LocalRawAssum ([],_,_) -> assert false
 
-let local_binders_loc bll =
-  if bll = [] then Loc.ghost else
-  Loc.merge (local_binder_loc (List.hd bll)) (local_binder_loc (List.last bll))
+let local_binders_loc bll = match bll with
+  | [] -> Loc.ghost
+  | h :: l ->
+    Loc.merge (local_binder_loc h) (local_binder_loc (List.last bll))
 
 (** Pseudo-constructors *)
 
-- 
cgit v1.2.3