diff options
| author |  msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-16 17:33:38 +0000 |
|---|---|---|
| committer | msozeau <msozeau@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2009-04-16 17:33:38 +0000 |
| commit | 491eb32c55c9b57a5a49ebbdc46f41ca5cb359c7 (patch) | |
| tree | 9a74d9ea6a65a10d9a80fde72027f0f809a9af18 /plugins/subtac/subtac.ml | |
| parent | 665761c4e82504a579d335b529b2e61f0414665c (diff) | |
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
Diffstat (limited to 'plugins/subtac/subtac.ml')
| -rw-r--r-- | plugins/subtac/subtac.ml | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/plugins/subtac/subtac.ml b/plugins/subtac/subtac.ml index d10c8f68c..36dc5f2ae 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 |