From 876b1b39a0304c93c2511ca8dd34353413e91c9d Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Tue, 12 Aug 2014 11:03:05 -0400 Subject: instanciation is French, instantiation is English --- library/universes.ml | 2 +- plugins/extraction/extraction.ml | 4 ++-- pretyping/typeclasses.ml | 8 ++++---- pretyping/typeclasses.mli | 4 ++-- tactics/class_tactics.ml | 8 ++++---- test-suite/success/unification.v | 2 +- theories/Classes/Morphisms_Relations.v | 2 +- theories/FSets/FMapAVL.v | 2 +- theories/Numbers/Rational/SpecViaQ/QSig.v | 2 +- 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 *) -- cgit v1.2.3