From c478daf2c33c03a812cbc2added4ce4ff7a9774a Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 1 Apr 2003 13:11:24 +0000
Subject: Fail 1 pour traverser le match

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

diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 97360dab2f..c1ba413f05 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -147,7 +147,7 @@ let field g =
     <:tactic<
       Match Context With
       | [|- (eq ?1 ?2 ?3)] -> Field_Gen FT
-      | _ -> Fail "Field: not an equality">>) g
+      | _ -> Fail 1 "Field: not an equality">>) g
 
 (* Verifies that all the terms have the same type and gives the right theory *)
 let guess_theory env evc = function
-- 
cgit v1.2.3