diff options
| author | Pierre-Marie Pédrot | 2015-10-15 09:47:43 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2015-10-15 09:47:43 +0200 |
| commit | cbd28511526dfb561017c3d27a73598f6ce5f68d (patch) | |
| tree | a8786b32433caa850e24f67ab5a3aa85f29a683a /plugins/decl_mode | |
| parent | 10e5883fed21f9631e1aa65adb7a7e62a529987f (diff) | |
| parent | 7402a7788b6a73bd5c0cb9078823d48e6f01a357 (diff) | |
Merge branch 'v8.5'
Diffstat (limited to 'plugins/decl_mode')
| -rw-r--r-- | plugins/decl_mode/decl_proof_instr.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/decl_mode/decl_proof_instr.ml b/plugins/decl_mode/decl_proof_instr.ml index f8ddd5f80c..d8c5b8a956 100644 --- a/plugins/decl_mode/decl_proof_instr.ml +++ b/plugins/decl_mode/decl_proof_instr.ml @@ -212,7 +212,7 @@ let close_previous_case pts = Proof.is_done pts then match get_top_stack pts with - Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occured ...") + Per (et,_,_,_) :: _ -> anomaly (Pp.str "Weird case occurred ...") | Suppose_case :: Per (et,_,_,_) :: _ -> goto_current_focus () | _ -> error "Not inside a proof per cases or induction." |