Orthographe de 'instantiate'

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

3 files changed, 4 insertions, 4 deletions

diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
index 9ad64e31d..b1f08a691 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 aec4c2fa3..9f9cc46a6 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 4f956ffc6..ec8fcd2a8 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. *)