From 06cd051d140a183229cd43f0bbae152d6ad8d6ca Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat
Date: Sun, 22 Jul 2018 18:19:26 -0400
Subject: Correct some spelling errors

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`.
---
 vernac/comProgramFixpoint.ml | 2 +-
 vernac/obligations.ml        | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'vernac')

diff --git a/vernac/comProgramFixpoint.ml b/vernac/comProgramFixpoint.ml
index ab898644c0..cea8af3f05 100644
--- a/vernac/comProgramFixpoint.ml
+++ b/vernac/comProgramFixpoint.ml
@@ -244,7 +244,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 bdf74bf63d..5352cf5f8c 100644
--- a/vernac/obligations.ml
+++ b/vernac/obligations.ml
@@ -348,7 +348,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; }
-- 
cgit v1.2.3