From cea2061080d540c0507192eca1887ea4b502680d Mon Sep 17 00:00:00 2001
From: herbelin
Date: Sat, 17 Dec 2005 21:07:17 +0000
Subject: Orthographe de 'instantiate'

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@7659 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 pretyping/clenv.mli   | 2 +-
 pretyping/evarconv.ml | 2 +-
 pretyping/evarutil.ml | 4 ++--
 3 files changed, 4 insertions(+), 4 deletions(-)

(limited to 'pretyping')

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. *)
 
-- 
cgit v1.2.3