From e53df7b8ea4542f84fd85dafc667511cc1252bc3 Mon Sep 17 00:00:00 2001
From: jforest
Date: Fri, 26 May 2006 08:10:33 +0000
Subject: removing a warning

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8862 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/recdef/recdef.ml4 | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index d918060746..ed2e5b5f50 100644
--- a/contrib/recdef/recdef.ml4
+++ b/contrib/recdef/recdef.ml4
@@ -311,8 +311,11 @@ let list_rewrite (rev:bool) (eqs: constr list) =
 let base_leaf_terminate (func:global_reference) eqs expr =
 (*  let _ = msgnl (str "entering base_leaf") in *)
   (fun g ->
-     
-     let [k';h] = pf_get_new_ids [k_id;h_id] g in 
+     let k',h = 
+       match pf_get_new_ids [k_id;h_id] g with 
+	   [k';h] -> k',h
+	 | _ -> assert false
+     in
      tclTHENLIST [observe_tac "first split" (split (ImplicitBindings [expr]));
 		  observe_tac "second split" (split (ImplicitBindings [delayed_force coq_O]));
 		  observe_tac "intro k" (h_intro k');
-- 
cgit v1.2.3