From bbceee6b20dd2bc17c2de537c2eb7bcc57700a23 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Wed, 15 May 2002 10:49:35 +0000
Subject: Contournement de la fermeture ML dans VContext

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

(limited to 'proofs/tacinterp.mli')

diff --git a/proofs/tacinterp.mli b/proofs/tacinterp.mli
index 0f52803446..188811c64c 100644
--- a/proofs/tacinterp.mli
+++ b/proofs/tacinterp.mli
@@ -23,7 +23,7 @@ type value =
   | VTactic of interp_sign * Coqast.t
   | VFTactic of tactic_arg list * string
   | VRTactic of (goal list sigma * validation)
-  | VContext of (interp_sign -> goal sigma -> value)
+  | VContext of interp_sign * Coqast.t * Coqast.t list
   | VArg of tactic_arg
   | VFun of (identifier * value) list * identifier option list * Coqast.t
   | VVoid
-- 
cgit v1.2.3