diff options
| author |  Benjamin Barenblat <bbaren@google.com> | 2018-07-22 18:19:26 -0400 |
|---|---|---|
| committer | Benjamin Barenblat <bbaren@google.com> | 2018-07-22 18:19:26 -0400 |
| commit | 234f5479773d43a48e67c5c0ea361445c7fb6782 (patch) | |
| tree | 0609f0aef4769561d3bee2049c5c973f40b20be3 /vernac | |
| parent | 32415df7e24d4d79a00fae95a5f619980b006c61 (diff) | |
Correct some spelling errorsmaster
Lintian found some spelling errors in the Debian packaging for coq. Fix
them most places they appear in the current source. (Don't change
documentation anchor names, as that would invalidate external
deeplinks.)
This also fixes a bug in coqdoc: prior to this commit, coqdoc would
highlight `instanciate` but not `instantiate`.
Diffstat (limited to 'vernac')
| -rw-r--r-- | vernac/comProgramFixpoint.ml | 2 | ||||
| -rw-r--r-- | vernac/obligations.ml | 2 |
2 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml index 102a98f04..ad21a6d9e 100644 --- a/vernac/comProgramFixpoint.ml +++ b/vernac/comProgramFixpoint.ml @@ -255,7 +255,7 @@ let do_program_recursive local poly fixkind fixl ntns = interp_recursive ~cofix ~program_mode:true fixl ntns in (* Program-specific code *) - (* Get the interesting evars, those that were not instanciated *) + (* Get the interesting evars, those that were not instantiated *) let evd = Typeclasses.resolve_typeclasses ~filter:Typeclasses.no_goals ~fail:true env evd in (* Solve remaining evars *) let evd = nf_evar_map_undefined evd in diff --git a/vernac/obligations.ml b/vernac/obligations.ml index 14d764232..abea7ff9d 100644 --- a/vernac/obligations.ml +++ b/vernac/obligations.ml @@ -342,7 +342,7 @@ open Goptions let _ = declare_bool_option { optdepr = false; - optname = "Hidding of Program obligations"; + optname = "Hiding of Program obligations"; optkey = ["Hide";"Obligations"]; optread = get_hide_obligations; optwrite = set_hide_obligations; } |