diff options
| author | Matej Kosik | 2017-02-03 09:02:19 +0100 |
|---|---|---|
| committer | Matej Košík | 2017-04-10 13:16:57 +0200 |
| commit | 28973285f4b9389ed0610b94ba907684214dd279 (patch) | |
| tree | 358fe7676d86b3d1fbe0980612640295b390eabc /engine | |
| parent | 9394aefa8e519a9e2b1b45659a47d5ff3f15ed16 (diff) | |
trivial
Diffstat (limited to 'engine')
| -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 721389af4f..acd931160f 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 } = 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 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 raw_concl { concl=concl } = concl + let raw_concl {concl} = concl let gmake_with info env sigma goal = |