From a3645985be17e9fa8a8a5c4221aea40e189682c2 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Mon, 14 Sep 2009 16:57:14 +0000
Subject: Backtrack on the forced discharge of type class variables introduced
 by Context. Now Context has exactly the same semantics as Variables.

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

(limited to 'plugins')

diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index 8b1d20e6de..b5e2880134 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -101,7 +101,7 @@ let declare_assumption env isevars idl is_coe k bl c nl =
       Subtac_pretyping.subtac_process env isevars id [] (Command.generalize_constr_expr c bl) None 
     in
     let c = solve_tccs_in_type env id isevars evm c typ in
-      List.iter (Command.declare_one_assumption is_coe k c imps false [] nl) idl
+      List.iter (Command.declare_one_assumption is_coe k c imps false nl) idl
   else
     errorlabstrm "Command.Assumption"
 	(str "Cannot declare an assumption while in proof editing mode.")
-- 
cgit v1.2.3