diff options
| author | Emilio Jesus Gallego Arias | 2018-10-15 15:31:27 +0200 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2018-10-15 15:31:27 +0200 |
| commit | fca9ec68937e047d3895d05e57de462387737796 (patch) | |
| tree | f6fc75f7e6be6b60ceafff3afa9d7e13b3219571 /plugins/funind/recdef.ml | |
| parent | b7dae2c97cce2a298bfbbd6f3a72a02e092ebe9e (diff) | |
| parent | 06cd051d140a183229cd43f0bbae152d6ad8d6ca (diff) | |
Merge PR #8589: Correct some spelling errors (continued)
Diffstat (limited to 'plugins/funind/recdef.ml')
| -rw-r--r-- | plugins/funind/recdef.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index 89dfb58017..9fa333c629 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -1320,7 +1320,7 @@ let open_new_goal build_proof sigma using_lemmas ref_ goal_name (gls_type,decomp | None -> try add_suffix current_proof_name "_subproof" with e when CErrors.noncritical e -> - anomaly (Pp.str "open_new_goal with an unamed theorem.") + anomaly (Pp.str "open_new_goal with an unnamed theorem.") in let na = next_global_ident_away name Id.Set.empty in if Termops.occur_existential sigma gls_type then |