diff options
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 8feb34e3e..594732a5a 100644 --- a/pretyping/unification.ml +++ b/pretyping/unification.ml @@ -480,8 +480,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 @@ -573,7 +573,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 |