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
---
 kernel/term.ml    | 2 +-
 kernel/typeops.ml | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'kernel')

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