diff options
Diffstat (limited to 'engine/proofview.ml')
| -rw-r--r-- | engine/proofview.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/engine/proofview.ml b/engine/proofview.ml index acd931160f..721389af4f 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -1019,13 +1019,13 @@ module Goal = struct let assume (gl : ('a, 'r) t) = (gl :> ([ `NF ], 'r) t) - let env {env} = env - let sigma {sigma} = Sigma.Unsafe.of_evar_map sigma - let hyps {env} = Environ.named_context env - let concl {concl} = concl - let extra {sigma; self} = goal_extra sigma self + let env { env=env } = env + let sigma { sigma=sigma } = Sigma.Unsafe.of_evar_map sigma + let hyps { env=env } = Environ.named_context env + let concl { concl=concl } = concl + let extra { sigma=sigma; self=self } = goal_extra sigma self - let raw_concl {concl} = concl + let raw_concl { concl=concl } = concl let gmake_with info env sigma goal = |