diff options
| -rw-r--r-- | library/lib.ml | 11 | ||||
| -rw-r--r-- | library/library.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 84 | ||||
| -rw-r--r-- | toplevel/vernac.ml | 12 |
4 files changed, 55 insertions, 54 deletions
diff --git a/library/lib.ml b/library/lib.ml index 40590a220..49e685f63 100644 --- a/library/lib.ml +++ b/library/lib.ml @@ -319,7 +319,7 @@ let end_compilation dir = | _, OpenedModtype _ -> error "There are some open module types" | _ -> assert false with - Not_found -> () + Not_found -> () in let module_p = function (_,CompilingLibrary _) -> true | x -> is_something_opened x @@ -331,16 +331,17 @@ let end_compilation dir = with Not_found -> anomaly "No module declared" in - let _ = match !comp_name with + let _ = + match !comp_name with | None -> anomaly "There should be a module name..." | Some m -> if m <> dir then anomaly ("The current open module has name "^ (string_of_dirpath m) ^ - " and not " ^ (string_of_dirpath m)); + " and not " ^ (string_of_dirpath m)); in let (after,_,before) = split_lib oname in - comp_name := None; - !path_prefix,after + comp_name := None; + !path_prefix,after (* Returns true if we are inside an opened module type *) let is_modtype () = diff --git a/library/library.ml b/library/library.ml index 73d58b549..2412f67a1 100644 --- a/library/library.ml +++ b/library/library.ml @@ -606,7 +606,7 @@ let save_library_to dir f = let di = Digest.file f' in System.marshal_out ch di; close_out ch - with e -> (warning ("Removed file "^f');close_out ch; Sys.remove f'; raise e) + with e -> (warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e) (************************************************************************) (*s Display the memory use of a library. *) diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index cfda82a98..1498fe018 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1617,52 +1617,52 @@ and interp_match_context ist g lz lr lmr = let rec apply_goal_sub ist env goal nocc (id,c) csr mt mhyps hyps = let (lgoal,ctxt) = match_subterm nocc c csr in let lctxt = give_context ctxt id in - try apply_hyps_context ist env lz goal mt lctxt lgoal mhyps hyps - with e when is_match_catchable e -> - apply_goal_sub ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in + try apply_hyps_context ist env lz goal mt lctxt lgoal mhyps hyps + with e when is_match_catchable e -> + apply_goal_sub ist env goal (nocc + 1) (id,c) csr mt mhyps hyps in let rec apply_match_context ist env goal nrs lex lpt = begin - if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex); - match lpt with - | (All t)::tl -> - begin - db_mc_pattern_success ist.debug; - try eval_with_fail ist lz goal t - with e when is_match_catchable e -> - apply_match_context ist env goal (nrs+1) (List.tl lex) tl - end - | (Pat (mhyps,mgoal,mt))::tl -> - let hyps = make_hyps (pf_hyps goal) in - let hyps = if lr then List.rev hyps else hyps in - let mhyps = List.rev mhyps (* Sens naturel *) in - let concl = pf_concl goal in - (match mgoal with - | Term mg -> - (try - let lgoal = matches mg concl in - db_matched_concl ist.debug (pf_env goal) concl; - apply_hyps_context ist env lz goal mt [] lgoal mhyps hyps - with e when is_match_catchable e -> - (match e with - | PatternMatchingFailure -> db_matching_failure ist.debug - | Eval_fail s -> db_eval_failure ist.debug s - | _ -> db_logic_failure ist.debug e); - apply_match_context ist env goal (nrs+1) (List.tl lex) tl) - | Subterm (id,mg) -> - (try apply_goal_sub ist env goal 0 (id,mg) concl mt mhyps hyps - with - | PatternMatchingFailure -> - apply_match_context ist env goal (nrs+1) (List.tl lex) tl)) - | _ -> - errorlabstrm "Tacinterp.apply_match_context" - (v 0 (str "No matching clauses for match goal" ++ - (if ist.debug=DebugOff then - fnl() ++ str "(use \"Debug On\" for more info)" - else mt()))) + if lex<>[] then db_pattern_rule ist.debug nrs (List.hd lex); + match lpt with + | (All t)::tl -> + begin + db_mc_pattern_success ist.debug; + try eval_with_fail ist lz goal t + with e when is_match_catchable e -> + apply_match_context ist env goal (nrs+1) (List.tl lex) tl + end + | (Pat (mhyps,mgoal,mt))::tl -> + let hyps = make_hyps (pf_hyps goal) in + let hyps = if lr then List.rev hyps else hyps in + let mhyps = List.rev mhyps (* Sens naturel *) in + let concl = pf_concl goal in + (match mgoal with + | Term mg -> + (try + let lgoal = matches mg concl in + db_matched_concl ist.debug (pf_env goal) concl; + apply_hyps_context ist env lz goal mt [] lgoal mhyps hyps + with e when is_match_catchable e -> + (match e with + | PatternMatchingFailure -> db_matching_failure ist.debug + | Eval_fail s -> db_eval_failure ist.debug s + | _ -> db_logic_failure ist.debug e); + apply_match_context ist env goal (nrs+1) (List.tl lex) tl) + | Subterm (id,mg) -> + (try apply_goal_sub ist env goal 0 (id,mg) concl mt mhyps hyps + with + | PatternMatchingFailure -> + apply_match_context ist env goal (nrs+1) (List.tl lex) tl)) + | _ -> + errorlabstrm "Tacinterp.apply_match_context" + (v 0 (str "No matching clauses for match goal" ++ + (if ist.debug=DebugOff then + fnl() ++ str "(use \"Debug On\" for more info)" + else mt()))) end in let env = pf_env g in - apply_match_context ist env g 0 lmr - (read_match_rule (fst (constr_list ist env)) lmr) + apply_match_context ist env g 0 lmr + (read_match_rule (fst (constr_list ist env)) lmr) (* Tries to match the hypotheses in a Match Context *) and apply_hyps_context ist env lz goal mt lctxt lgmatch mhyps hyps = diff --git a/toplevel/vernac.ml b/toplevel/vernac.ml index f3bc0793f..746a9a9f4 100644 --- a/toplevel/vernac.ml +++ b/toplevel/vernac.ml @@ -162,12 +162,12 @@ let rec vernac_com interpfun (loc,com) = | v -> if not !just_parsing then interpfun v in - try - if do_translate () then pr_new_syntax loc (Some com); - interp com - with e -> - Format.set_formatter_out_channel stdout; - raise (DuringCommandInterp (loc, e)) + try + if do_translate () then pr_new_syntax loc (Some com); + interp com + with e -> + Format.set_formatter_out_channel stdout; + raise (DuringCommandInterp (loc, e)) and vernac interpfun input = vernac_com interpfun (parse_phrase input) |