diff options
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/lemmas.ml | 2 | ||||
| -rw-r--r-- | vernac/obligations.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/vernac/lemmas.ml b/vernac/lemmas.ml index d6ae0ea86f..045eed3e19 100644 --- a/vernac/lemmas.ml +++ b/vernac/lemmas.ml @@ -169,7 +169,7 @@ let look_for_possibly_mutual_statements = function let recguard,ordered_inds = find_mutually_recursive_statements thms in let thms = List.map pi2 ordered_inds in Some recguard,thms, Some (List.map (fun (_,_,i) -> succ i) ordered_inds) - | [] -> anomaly (Pp.str "Empty list of theorems.") + | [] -> anomaly (Pp.str "Empty list of theorems") (* Saving a goal *) diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 47ac16f9c7..b0b35aed50 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -1166,7 +1166,7 @@ let next_obligation n tac = let is_open _ x = Option.is_empty x.obl_body && List.is_empty (deps_remaining obls x.obl_deps) in let i = match Array.findi is_open obls with | Some i -> i - | None -> anomaly (Pp.str "Could not find a solvable obligation.") + | None -> anomaly (Pp.str "Could not find a solvable obligation") in solve_obligation prg i tac |