diff options
| author | Pierre-Marie Pédrot | 2016-11-08 10:57:05 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-02-14 17:27:23 +0100 |
| commit | 67dc22d8389234d0c9b329944ff579e7056b7250 (patch) | |
| tree | 4b0d94384103f34e8b6071a214efb84904a56277 /ltac | |
| parent | e4f066238799a4598817dfeab8a044760ab670de (diff) | |
Cases API using EConstr.
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/rewrite.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index 0091d0d0a8..58153c4534 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -344,7 +344,7 @@ end) = struct Some (evars, found, c, ty, arg :: args) with Not_found -> let ty = whd_all env ty in - find env (mkApp (c, [| arg |])) (prod_applist ty [arg]) args + find env (mkApp (c, [| arg |])) (Term.prod_applist ty [arg]) args in find env c ty args let unlift_cstr env sigma = function |