From 4e06ff81b384ab51009abfeede8bce5f95f2bf39 Mon Sep 17 00:00:00 2001
From: notin
Date: Thu, 16 Aug 2007 11:16:43 +0000
Subject: Correction du bug #1680: ajout d'un champ avoid_ids dans interp_sign;
 modification de interp_ltac_reference pour passer les ids utilisées dans le
 contexte d'appel d'une tactique.

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

(limited to 'contrib/field')

diff --git a/contrib/field/field.ml4 b/contrib/field/field.ml4
index b8a978d84e..93de6118b6 100644
--- a/contrib/field/field.ml4
+++ b/contrib/field/field.ml4
@@ -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