Orthographe de 'instantiate'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7659 85f007b7-540e-0410-9357-904b9bb8a0f7

6 files changed, 8 insertions, 8 deletions

diff --git a/kernel/term.ml b/kernel/term.ml
index f59ba5d66f..5bbe372e42 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -8,7 +8,7 @@
 
 (* $Id$ *)
 
-(* This module instanciates the structure of generic deBruijn terms to Coq *)
+(* This module instantiates the structure of generic deBruijn terms to Coq *)
 
 open Util
 open Pp
diff --git a/kernel/typeops.ml b/kernel/typeops.ml
index 3a968545f2..89a1c19826 100644
--- a/kernel/typeops.ml
+++ b/kernel/typeops.ml
@@ -106,7 +106,7 @@ let judge_of_variable env id =
 
 (* Management of context of variables. *)
 
-(* Checks if a context of variable can be instanciated by the
+(* Checks if a context of variable can be instantiated by the
    variables of the current env *)
 (* TODO: check order? *)
 let rec check_hyps_inclusion env sign =
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 9ad64e31da..b1f08a6916 100644
--- a/pretyping/clenv.mli
+++ b/pretyping/clenv.mli
@@ -28,7 +28,7 @@ open Mod_subst
  * [templval] is the template which we are trying to fill out.
  * [templtyp] is its type.
  * [namenv] is a mapping from metavar numbers to names, for
- *          use in instanciating metavars by name.
+ *          use in instantiating metavars by name.
  *)
 type clausenv = {
   templenv : env;
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index aec4c2fa3a..9f9cc46a66 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -127,7 +127,7 @@ let check_conv_record (t1,l1) (t2,l2) =
     raise Not_found
 
 
-(* Precondition: one of the terms of the pb is an uninstanciated evar,
+(* Precondition: one of the terms of the pb is an uninstantiated evar,
  * possibly applied to arguments. *)
 
 let rec ise_try isevars = function
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index 4f956ffc6c..ec8fcd2a8c 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -319,7 +319,7 @@ let do_restrict_hyps evd ev args =
 
 let need_restriction isevars args = not (array_for_all closed0 args)
 
-(* We try to instanciate the evar assuming the body won't depend
+(* We try to instantiate the evar assuming the body won't depend
  * on arguments that are not Rels or Vars, or appearing several times.
  *)
 (* Note: error_not_clean should not be an error: it simply means that the
@@ -513,7 +513,7 @@ let solve_refl conv_algo env isevars ev argsv1 argsv2 =
 
 
 (* Tries to solve problem t1 = t2.
- * Precondition: t1 is an uninstanciated evar
+ * Precondition: t1 is an uninstantiated evar
  * Returns an optional list of evars that were instantiated, or None
  * if the problem couldn't be solved. *)
 
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 0c916f7038..f64bae5a19 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -221,7 +221,7 @@ let declare_one_elimination ind =
   let sigma = Evd.empty in
   let elim_scheme = Indrec.build_indrec env sigma ind in
   let npars = mib.mind_nparams_rec in
-  let make_elim s = Indrec.instanciate_indrec_scheme s npars elim_scheme in
+  let make_elim s = Indrec.instantiate_indrec_scheme s npars elim_scheme in
   let kelim = mip.mind_kelim in
   (* in case the inductive has a type elimination, generates only one
      induction scheme, the other ones share the same code with the
@@ -232,7 +232,7 @@ let declare_one_elimination ind =
     let c = mkConst cte and t = constant_type (Global.env()) cte in
     List.iter (fun (sort,suff) -> 
       let (t',c') = 
-	Indrec.instanciate_type_indrec_scheme (new_sort_in_family sort)
+	Indrec.instantiate_type_indrec_scheme (new_sort_in_family sort)
 	  npars c t in
       let _ = declare (mindstr^suff) c' (Some t') in ())
       non_type_eliminations