diff options
Diffstat (limited to 'tactics/leminv.ml')
| -rw-r--r-- | tactics/leminv.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/leminv.ml b/tactics/leminv.ml index 2a2a1e356..19e7153b5 100644 --- a/tactics/leminv.ml +++ b/tactics/leminv.ml @@ -156,7 +156,7 @@ let compute_first_inversion_scheme env sigma ind sort dep_option = let revargs,ownsign = fold_named_context (fun env (id,_,_ as d) (revargs,hyps) -> - if List.mem id ivars then + if Id.List.mem id ivars then ((mkVar id)::revargs,add_named_decl d hyps) else (revargs,hyps)) |