aboutsummaryrefslogtreecommitdiff
path: root/vernac/comProgramFixpoint.ml
diff options
context:
space:
mode:
authorEmilio Jesus Gallego Arias2018-10-15 15:31:27 +0200
committerEmilio Jesus Gallego Arias2018-10-15 15:31:27 +0200
commitfca9ec68937e047d3895d05e57de462387737796 (patch)
treef6fc75f7e6be6b60ceafff3afa9d7e13b3219571 /vernac/comProgramFixpoint.ml
parentb7dae2c97cce2a298bfbbd6f3a72a02e092ebe9e (diff)
parent06cd051d140a183229cd43f0bbae152d6ad8d6ca (diff)
Merge PR #8589: Correct some spelling errors (continued)
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