diff options
author | Matthieu Sozeau <mattam@mattam.org> | 2016-09-12 13:37:08 +0200 |
---|---|---|
committer | Matthieu Sozeau <mattam@mattam.org> | 2016-09-12 13:37:08 +0200 |
commit | 7a3ef81f20e159bcf4d40227d36c54abbe69c3e9 (patch) | |
tree | 1527039fb27481b1ce82e2d3cff8fa82ce834ce3 /pretyping/unification.ml | |
parent | 12cedcbf4dcfe4fd43ab9f4b648314cac26b82db (diff) | |
parent | 43869b4e05824244e666c60e0b740a80e8b09d0c (diff) |
Merge remote-tracking branch 'github-coq/pr/249' into v8.6
Diffstat (limited to 'pretyping/unification.ml')
-rw-r--r-- | pretyping/unification.ml | 7 |
1 files changed, 4 insertions, 3 deletions
diff --git a/pretyping/unification.ml b/pretyping/unification.ml index 6d80db645..bc888b897 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -479,8 +479,8 @@ let unfold_projection env p stk = let expand_key ts env sigma = function | Some (IsKey k) -> expand_table_key env k | Some (IsProj (p, c)) -> - let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma - Cst_stack.empty (c, unfold_projection env p []))) + let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma + Cst_stack.empty (c, unfold_projection env p []))) in if Term.eq_constr (mkProj (p, c)) red then None else Some red | None -> None @@ -572,7 +572,8 @@ let constr_cmp pb sigma flags t u = else sigma, b let do_reduce ts (env, nb) sigma c = - Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma Cst_stack.empty (c, Stack.empty))) + Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state + ts env sigma Cst_stack.empty (c, Stack.empty))) let use_full_betaiota flags = flags.modulo_betaiota && Flags.version_strictly_greater Flags.V8_3 |