From 491eb32c55c9b57a5a49ebbdc46f41ca5cb359c7 Mon Sep 17 00:00:00 2001
From: msozeau
Date: Thu, 16 Apr 2009 17:33:38 +0000
Subject: Better Requires in Classes. Fix bug #2093: the code does not require
 Program.Tactics anymore.

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

(limited to 'plugins')

diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml
index d10c8f68c2..36dc5f2ae7 100644
--- a/plugins/subtac/subtac.ml
+++ b/plugins/subtac/subtac.ml
@@ -54,8 +54,8 @@ let solve_tccs_in_type env id isevars evm c typ =
     let stmt_id = Nameops.add_suffix id "_stmt" in
     let obls, c', t' = eterm_obligations env stmt_id !isevars evm 0 ~status:Expand c typ in
       match Subtac_obligations.add_definition stmt_id c' typ obls with
-      Subtac_obligations.Defined cst -> constant_value (Global.env()) 
-	(match cst with ConstRef kn -> kn | _ -> assert false)
+      | Subtac_obligations.Defined cst -> constant_value (Global.env()) 
+	  (match cst with ConstRef kn -> kn | _ -> assert false)
       | _ -> 
 	  errorlabstrm "start_proof" 
 	    (str "The statement obligations could not be resolved automatically, " ++ spc () ++
@@ -127,7 +127,6 @@ let check_fresh (loc,id) =
 let subtac (loc, command) =
   check_required_library ["Coq";"Init";"Datatypes"];
   check_required_library ["Coq";"Init";"Specif"];
-  check_required_library ["Coq";"Program";"Tactics"];
   let env = Global.env () in
   let isevars = ref (create_evar_defs Evd.empty) in
   try
-- 
cgit v1.2.3