From 4f3a7b740b7969c44a75c5620bf118e43c5d8b62 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Thu, 8 Jun 2006 08:00:23 +0000
Subject: Détection bug rawwit suitecorrection trou de typage create_arg

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

diff --git a/contrib/interface/xlate.ml b/contrib/interface/xlate.ml
index deb8426658..585e4bfb65 100644
--- a/contrib/interface/xlate.ml
+++ b/contrib/interface/xlate.ml
@@ -1102,7 +1102,7 @@ and xlate_tac =
 				  List.map (fun x -> CT_ident x) l))))
     | TacExtend (_,"prolog", [cl; n]) ->
       let cl = List.map xlate_formula (out_gen (wit_list0 rawwit_constr) cl) in
-      (match out_gen wit_int_or_var n with
+      (match out_gen rawwit_int_or_var n with
 	| ArgVar _ -> xlate_error ""
 	| ArgArg n -> CT_prolog (CT_formula_list cl, CT_int  n))
     | TacExtend (_,"eapply", [cbindl]) ->
-- 
cgit v1.2.3