diff options
Diffstat (limited to 'contrib')
| -rw-r--r-- | contrib/ring/quote.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/contrib/ring/quote.ml b/contrib/ring/quote.ml index 10c05ec0e3..669fd21c50 100644 --- a/contrib/ring/quote.ml +++ b/contrib/ring/quote.ml @@ -268,7 +268,7 @@ let compute_ivs gl f cs = (* The Cases predicate is a lambda; we assume no dependency *) let p = match kind_of_term p with - | Lambda (_,_,p) -> pop p + | Lambda (_,_,p) -> Termops.pop p | _ -> p in |