From af08be9e326fe4b7e76234022fe33b1eea4c06dd Mon Sep 17 00:00:00 2001
From: herbelin
Date: Mon, 22 Sep 2003 07:28:03 +0000
Subject: Passage à la V8 par défaut

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4437 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 contrib/field/field.ml4          | 2 +-
 contrib/first-order/g_ground.ml4 | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'contrib')

diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index 68650ce04a..57b8cd750f 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -156,7 +156,7 @@ let field g =
       | _ -> error "The statement is not built from Leibniz' equality" in
   let th = VConstr (lookup (pf_env g) typ) in
   (interp_tac_gen [(id_of_string "FT",th)] (get_debug ())
-    <:tactic< Match Context With [|-(!eq ? ? ?)] -> Field_Gen FT>>) g
+    <:tactic< match context with [|- (@eq _ _ _) ] => Field_Gen FT end >>) g
 
 (* Verifies that all the terms have the same type and gives the right theory *)
 let guess_theory env evc = function
diff --git a/contrib/first-order/g_ground.ml4 b/contrib/first-order/g_ground.ml4
index 95b162d288..33e4107f65 100644
--- a/contrib/first-order/g_ground.ml4
+++ b/contrib/first-order/g_ground.ml4
@@ -39,7 +39,7 @@ let _=
   in
     declare_int_option gdopt
       
-let default_solver=(Tacinterp.interp <:tactic<Auto with *>>)
+let default_solver=(Tacinterp.interp <:tactic<auto with *>>)
     
 let fail_solver=tclFAIL 0 "GTauto failed"
 		      
-- 
cgit v1.2.3