diff options
| author | Maxime Dénès | 2016-07-01 17:24:12 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2016-07-01 17:26:08 +0200 |
| commit | 500d38d0887febb614ddcadebaef81e0c7942584 (patch) | |
| tree | 6ca260dfda3b6d95ff26be24e39010e2c82f881d /ltac | |
| parent | 9501ddd635adea7db07b4df60b8bda1d557dff18 (diff) | |
| parent | 1b09098cc4830f262820d2935a9cd0afa383ed3f (diff) | |
Merge branch 'reduction-flags' into trunk
Was PR#231: Separate flags for fix/cofix/match reduction and clean reduction
function names, itself a revision of PR#117: Isolating flags for cofix/fix
reduction + adjusting names of reduction functions to what they do
Diffstat (limited to 'ltac')
| -rw-r--r-- | ltac/rewrite.ml | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/ltac/rewrite.ml b/ltac/rewrite.ml index cb39df8ab5..0b01eeef4d 100644 --- a/ltac/rewrite.ml +++ b/ltac/rewrite.ml @@ -218,7 +218,7 @@ end) = struct | Some (x, Some rel) -> evars, rel in let rec aux env evars ty l = - let t = Reductionops.whd_betadeltaiota env (goalevars evars) ty in + let t = Reductionops.whd_all env (goalevars evars) ty in match kind_of_term t, l with | Prod (na, ty, b), obj :: cstrs -> let b = Reductionops.nf_betaiota (goalevars evars) b in @@ -321,7 +321,7 @@ end) = struct let rec aux evars env prod n = if Int.equal n 0 then start evars env prod else - match kind_of_term (Reduction.whd_betadeltaiota env prod) with + match kind_of_term (Reduction.whd_all env prod) with | Prod (na, ty, b) -> if noccurn 1 b then let b' = lift (-1) b in @@ -339,7 +339,7 @@ end) = struct try let evars, found = aux evars env ty (succ (List.length args)) in Some (evars, found, c, ty, arg :: args) with Not_found -> - let ty = whd_betadeltaiota env ty in + let ty = whd_all env ty in find env (mkApp (c, [| arg |])) (prod_applist ty [arg]) args in find env c ty args |