diff options
Diffstat (limited to 'tactics/inv.ml')
| -rw-r--r-- | tactics/inv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/inv.ml b/tactics/inv.ml index d1d6178da..0b2d2f0b2 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -443,7 +443,7 @@ let raw_inversion inv_kind id status names = let msg = str "The type of " ++ pr_id id ++ str " is not inductive." in CErrors.user_err msg in - let IndType (indf,realargs) = find_rectype env sigma t in + let IndType (indf,realargs) = find_rectype env sigma (EConstr.of_constr t) in let evdref = ref sigma in let (elim_predicate, args) = make_inv_predicate env evdref indf realargs id status concl in |