diff options
Diffstat (limited to 'mathcomp/ssreflect/plugin')
| -rw-r--r-- | mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 index 2b958b5..8817d82 100644 --- a/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 +++ b/mathcomp/ssreflect/plugin/v8.5/ssreflect.ml4 @@ -4130,7 +4130,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 *) |