diff options
Diffstat (limited to 'tactics/elim.ml')
| -rw-r--r-- | tactics/elim.ml | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/tactics/elim.ml b/tactics/elim.ml index fed756814..a79186719 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -12,9 +12,10 @@ open Pp open Util open Names open Term +open Termops open Environ open Reduction -open Inductive +open Inductiveops open Proof_type open Clenv open Hipattern @@ -104,7 +105,7 @@ let inductive_of_qualid gls qid = with Not_found -> Nametab.error_global_not_found qid in match kind_of_term c with - | IsMutInd ity -> ity + | Ind ity -> ity | _ -> errorlabstrm "Decompose" [< Nametab.pr_qualid qid; 'sTR " is not an inductive type" >] |