From d671e577800f450633ec9f13dc857f1af804a90a Mon Sep 17 00:00:00 2001
From: thery
Date: Thu, 18 Feb 2016 00:55:29 +0100
Subject: typo in error message

---
 mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 2 +-
 mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4  | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'mathcomp')

diff --git a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
index 1c335f4..f0b6306 100644
--- a/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/trunk/ssreflect.ml4
@@ -4165,7 +4165,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
       let pat = List.find (fun t -> Intset.mem i (evars_of_term t)) patterns in
       errorstrm(str"Pattern"++spc()++pr_constr_pat pat++spc()++
         str"was not completely instantiated and one of its variables"++spc()++
-        str"occurs in the type of another non instantieted pattern variable");
+        str"occurs in the type of another non-instantiated pattern variable");
     end
   in
   (* the elim tactic, with the eliminator and the predicated we computed *)
diff --git a/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4
index 1c22477..23b4ae5 100644
--- a/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4
+++ b/mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4
@@ -4046,7 +4046,7 @@ let ssrelim ?(is_case=false) ?ist deps what ?elim eqid ipats gl =
       let pat = List.find (fun t -> Intset.mem i (evars_of_term t)) patterns in
       errorstrm(str"Pattern"++spc()++pr_constr_pat pat++spc()++
         str"was not completely instantiated and one of its variables"++spc()++
-        str"occurs in the type of another non instantieted pattern variable");
+        str"occurs in the type of another non-instantiated pattern variable");
     end
   in
   (* the elim tactic, with the eliminator and the predicated we computed *)
-- 
cgit v1.2.3