removing a warning

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8862 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 5 insertions, 2 deletions

diff --git a/contrib/recdef/recdef.ml4 b/contrib/recdef/recdef.ml4
index d91806074..ed2e5b5f5 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');