instanciation is French, instantiation is English

9 files changed, 17 insertions, 17 deletions

diff --git a/library/universes.ml b/library/universes.ml
index b6c891c2f..a3be640ff 100644
--- a/library/universes.ml
+++ b/library/universes.ml
@@ -805,7 +805,7 @@ let normalize_context_set ctx us algs =
       in (noneqs, ucstrsl', ucstrsr'))
     noneqs (Constraint.empty, LMap.empty, LMap.empty)
   in
-  (* Now we construct the instanciation of each variable. *)
+  (* Now we construct the instantiation of each variable. *)
   let ctx', us, algs, inst, noneqs = 
     minimize_univ_variables ctx us algs ucstrsr ucstrsl noneqs
   in
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index 618717cde..498b33b63 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -56,8 +56,8 @@ let sort_of env c =
      More formally, a type scheme has type $(x_1:X_1)\ldots(x_n:X_n)s$ with
      [s = Set], [Prop] or [Type]
    \item [Default] denotes the other cases. It may be inexact after
-     instanciation. For example [(X:Type)X] is [Default] and may give [Set]
-     after instanciation, which is rather [TypeScheme]
+     instantiation. For example [(X:Type)X] is [Default] and may give [Set]
+     after instantiation, which is rather [TypeScheme]
    \item [Logic] denotes a term of sort [Prop], or a type scheme on sort [Prop]
    \item [Info] is the opposite. The same example [(X:Type)X] shows
      that an [Info] term might in fact be [Logic] later on.
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index 67189e22d..b9c2bd1bb 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -32,10 +32,10 @@ let set_typeclass_transparency gr local c = Hook.get set_typeclass_transparency
 let (classes_transparent_state, classes_transparent_state_hook) = Hook.make ()
 let classes_transparent_state () = Hook.get classes_transparent_state ()
 
-let solve_instanciation_problem = ref (fun _ _ _ -> assert false)
+let solve_instantiation_problem = ref (fun _ _ _ -> assert false)
 
 let resolve_one_typeclass env evm t =
-  !solve_instanciation_problem env evm t
+  !solve_instantiation_problem env evm t
 
 type direction = Forward | Backward
 
@@ -552,10 +552,10 @@ let has_typeclasses filter evd =
   in
   Evar.Map.exists check (Evd.undefined_map evd)
 
-let solve_instanciations_problem = ref (fun _ _ _ _ _ -> assert false)
+let solve_instantiations_problem = ref (fun _ _ _ _ _ -> assert false)
 
 let solve_problem env evd filter split fail =
-  !solve_instanciations_problem env evd filter split fail
+  !solve_instantiations_problem env evd filter split fail
 
 (** Profiling resolution of typeclasses *)
 (* let solve_classeskey = Profile.declare_profile "solve_typeclasses" *)
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index 295a092a8..7c3d2be09 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -119,8 +119,8 @@ val add_instance_hint : global_reference_or_constr -> global_reference list ->
   bool -> int option -> Decl_kinds.polymorphic -> unit
 val remove_instance_hint : global_reference -> unit
 
-val solve_instanciations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> evar_map) ref
-val solve_instanciation_problem : (env -> evar_map -> types -> open_constr) ref
+val solve_instantiations_problem : (env -> evar_map -> evar_filter -> bool -> bool -> evar_map) ref
+val solve_instantiation_problem : (env -> evar_map -> types -> open_constr) ref
 
 val declare_instance : int option -> bool -> global_reference -> unit
 
diff --git a/tactics/class_tactics.ml b/tactics/class_tactics.ml
index 9cf5aec04..1160884c3 100644
--- a/tactics/class_tactics.ml
+++ b/tactics/class_tactics.ml
@@ -559,7 +559,7 @@ let resolve_one_typeclass env ?(sigma=Evd.empty) gl =
     evd, term
 
 let _ =
-  Typeclasses.solve_instanciation_problem := (fun x y z -> resolve_one_typeclass x ~sigma:y z)
+  Typeclasses.solve_instantiation_problem := (fun x y z -> resolve_one_typeclass x ~sigma:y z)
 
 (** [split_evars] returns groups of undefined evars according to dependencies *)
 
@@ -688,16 +688,16 @@ let solve_inst debug depth env evd filter split fail =
   resolve_typeclass_evars debug depth env evd filter split fail
 
 let _ =
-  Typeclasses.solve_instanciations_problem :=
+  Typeclasses.solve_instantiations_problem :=
     solve_inst false !typeclasses_depth
 
 let set_typeclasses_debug d = (:=) typeclasses_debug d;
-  Typeclasses.solve_instanciations_problem := solve_inst d !typeclasses_depth
+  Typeclasses.solve_instantiations_problem := solve_inst d !typeclasses_depth
 
 let get_typeclasses_debug () = !typeclasses_debug
 
 let set_typeclasses_depth d = (:=) typeclasses_depth d;
-  Typeclasses.solve_instanciations_problem := solve_inst !typeclasses_debug !typeclasses_depth
+  Typeclasses.solve_instantiations_problem := solve_inst !typeclasses_debug !typeclasses_depth
 
 let get_typeclasses_depth () = !typeclasses_depth
 
diff --git a/test-suite/success/unification.v b/test-suite/success/unification.v
index 249079294..296686e16 100644
--- a/test-suite/success/unification.v
+++ b/test-suite/success/unification.v
@@ -101,7 +101,7 @@ apply H.
 Qed.
 
 (* Feature deactivated in commit 14189 (see commit log)
-(* Test instanciation of evars by unification *)
+(* Test instantiation of evars by unification *)
 
 Goal (forall x, 0 + x = 0 -> True) -> True.
 intros; eapply H.
diff --git a/theories/Classes/Morphisms_Relations.v b/theories/Classes/Morphisms_Relations.v
index dc46b4bbb..44e4808b8 100644
--- a/theories/Classes/Morphisms_Relations.v
+++ b/theories/Classes/Morphisms_Relations.v
@@ -38,7 +38,7 @@ Lemma predicate_implication_pointwise (l : Tlist) :
   Proper (@predicate_implication l ==> pointwise_lifting impl l) id.
 Proof. do 2 red. unfold predicate_implication. auto. Qed.
 
-(** The instanciation at relation allows to rewrite applications of relations
+(** The instantiation at relation allows to rewrite applications of relations
     [R x y] to [R' x y]  when [R] and [R'] are in [relation_equivalence]. *)
 
 Instance relation_equivalence_pointwise :
diff --git a/theories/FSets/FMapAVL.v b/theories/FSets/FMapAVL.v
index fa33c1bf4..fe08960ad 100644
--- a/theories/FSets/FMapAVL.v
+++ b/theories/FSets/FMapAVL.v
@@ -270,7 +270,7 @@ Fixpoint elements_aux (acc : list (key*elt)) m : list (key*elt) :=
    | Node l x d r _ => elements_aux ((x,d) :: elements_aux acc r) l
   end.
 
-(** then [elements] is an instanciation with an empty [acc] *)
+(** then [elements] is an instantiation with an empty [acc] *)
 
 Definition elements := elements_aux nil.
 
diff --git a/theories/Numbers/Rational/SpecViaQ/QSig.v b/theories/Numbers/Rational/SpecViaQ/QSig.v
index e199c7135..21d714ea1 100644
--- a/theories/Numbers/Rational/SpecViaQ/QSig.v
+++ b/theories/Numbers/Rational/SpecViaQ/QSig.v
@@ -104,7 +104,7 @@ Ltac qify := unfold eq, lt, le in *; autorewrite with qsimpl;
  try rewrite spec_0 in *; try rewrite spec_1 in *; try rewrite spec_m1 in *.
 
 (** NB: do not add [spec_0] in the autorewrite database. Otherwise,
-    after instanciation in BigQ, this lemma become convertible to 0=0,
+    after instantiation in BigQ, this lemma become convertible to 0=0,
     and autorewrite loops. Idem for [spec_1] and [spec_m1] *)
 
 (** Morphisms *)