From a0cfa4f118023d35b767a999d5a2ac4b082857b4 Mon Sep 17 00:00:00 2001
From: Samuel Mimram <smimram@debian.org>
Date: Fri, 25 Jul 2008 15:12:53 +0200
Subject: Imported Upstream version 8.2~beta3+dfsg

---
 contrib/field/field.ml4 | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'contrib/field/field.ml4')

diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index dab5a45c..dea79773 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -8,7 +8,7 @@
 
 (*i camlp4deps: "parsing/grammar.cma" i*)
 
-(* $Id: field.ml4 9273 2006-10-25 11:30:36Z barras $ *)
+(* $Id: field.ml4 10076 2007-08-16 11:16:43Z notin $ *)
 
 open Names
 open Pp
@@ -159,7 +159,7 @@ let field g =
       | Some (eq,t::args) when eq = (Coqlib.build_coq_eq_data()).Coqlib.eq -> t
       | _ -> 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 ())
+  (interp_tac_gen [(id_of_string "FT",th)] [] (get_debug ())
     <:tactic< match goal with |- (@eq _ _ _) => field_gen FT end >>) g
 
 (* Verifies that all the terms have the same type and gives the right theory *)
-- 
cgit v1.2.3