diff options
| author | Matej Košík | 2017-04-10 16:03:43 +0200 |
|---|---|---|
| committer | Matej Košík | 2017-04-10 16:03:43 +0200 |
| commit | 5984a068dc576c96f594be255630036c40afa55e (patch) | |
| tree | e5a366890fc2dac944d20cec49896f86e5971f75 /engine | |
| parent | e248b3d45835695c3bcf7c60e80172919025cd64 (diff) | |
Revert "trivial"
This reverts commit 28973285f4b9389ed0610b94ba907684214dd279.
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 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 = |