diff options
| author | Hugo Herbelin | 2019-05-25 19:21:49 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-06-16 14:04:19 +0200 |
| commit | e034b4090ca45410853db60ae2a5d2f220b48792 (patch) | |
| tree | c6f3476741850b4092c789f8bc9c8b3b2940b29d /vernac/comAssumption.ml | |
| parent | f95017c2c69ee258ae570b789bce696357d2c365 (diff) | |
Turning "manual_implicits" into a list of position in impargs.ml.
Diffstat (limited to 'vernac/comAssumption.ml')
| -rw-r--r-- | vernac/comAssumption.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/vernac/comAssumption.ml b/vernac/comAssumption.ml index c1f676b043..a27c08d176 100644 --- a/vernac/comAssumption.ml +++ b/vernac/comAssumption.ml @@ -283,8 +283,8 @@ let context poly l = Classes.declare_instance env sigma (Some Hints.empty_hint_info) true (ConstRef cst); status else - let test {CAst.v = (x, _)} = match x with - | Constrexpr.ExplByPos (_, Some id') -> Id.equal id id' + let test x = match x.CAst.v with + | Some (Name id',_) -> Id.equal id id' | _ -> false in let impl = List.exists test impls in |