diff options
Diffstat (limited to 'tactics/elim.ml')
| -rw-r--r-- | tactics/elim.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index a79186719..1b56914e9 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -108,7 +108,7 @@ let inductive_of_qualid gls qid = | Ind ity -> ity | _ -> errorlabstrm "Decompose" - [< Nametab.pr_qualid qid; 'sTR " is not an inductive type" >] + (Nametab.pr_qualid qid ++ str " is not an inductive type") let decompose_these c l gls = let indl = List.map (inductive_of_qualid gls) l in |