aboutsummaryrefslogtreecommitdiff
path: root/vernac/comProgramFixpoint.ml
diff options
context:
space:
mode:
authorBenjamin Barenblat2018-07-22 18:19:26 -0400
committerHugo Herbelin2018-10-15 13:28:52 +0200
commit06cd051d140a183229cd43f0bbae152d6ad8d6ca (patch)
tree6528aa85924d1cfdb965b81a15b4ec93189554fa /vernac/comProgramFixpoint.ml
parentecf999c8f8a677508d2856c3c8a7cacfa5da3839 (diff)
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`.
Diffstat (limited to 'vernac/comProgramFixpoint.ml')
-rw-r--r--vernac/comProgramFixpoint.ml2
1 files changed, 1 insertions, 1 deletions
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