diff options
Diffstat (limited to 'contrib/subtac/subtac.ml')
| -rw-r--r-- | contrib/subtac/subtac.ml | 14 |
1 files changed, 5 insertions, 9 deletions
diff --git a/contrib/subtac/subtac.ml b/contrib/subtac/subtac.ml index ba00fce5..c0b64379 100644 --- a/contrib/subtac/subtac.ml +++ b/contrib/subtac/subtac.ml @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(* $Id: subtac.ml 11800 2009-01-18 18:34:15Z msozeau $ *) +(* $Id: subtac.ml 12194 2009-06-17 16:38:09Z msozeau $ *) open Global open Pp @@ -99,7 +99,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 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.") @@ -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 @@ -143,7 +142,7 @@ let subtac (loc, command) = start_proof_and_print env isevars (Some lid) (Global, DefinitionBody Definition) (bl,t) (fun _ _ -> ()) | DefineBody (bl, _, c, tycon) -> - ignore(Subtac_pretyping.subtac_proof defkind env isevars id bl c tycon)) + ignore(Subtac_pretyping.subtac_proof defkind hook env isevars id bl c tycon)) | VernacFixpoint (l, b) -> List.iter (fun ((lid, _, _, _, _), _) -> check_fresh lid; @@ -237,9 +236,6 @@ let subtac (loc, command) = debug 2 (Himsg.explain_pretype_error env exn); raise e - | e'' -> msg_warning (str "Unexpected exception: " ++ Cerrors.explain_exn e''); - raise e) + | e'' -> raise e) - | e -> - msg_warning (str "Uncatched exception: " ++ Cerrors.explain_exn e); - raise e + | e -> raise e |