diff options
| author | thery | 2016-02-18 00:55:29 +0100 |
|---|---|---|
| committer | thery | 2016-02-18 00:55:29 +0100 |
| commit | 6e60581dcff29eca5885361dcea0d9611a5043ad (patch) | |
| tree | 7acfb02e372dd079e7ea6e40e38560c8a11f4713 | |
| parent | 80ba26baaf0581407e401f56d83cb59bd090db53 (diff) | |
type in error message
| -rw-r--r-- | mathcomp/ssreflect/plugin/trunk/ssreflect.ml4 | 2 | ||||
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.4/ssreflect.ml4 | 2 |
2 files changed, 2 insertions, 2 deletions
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 *) |