aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/patternops.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-12-06 18:02:56 +0100
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2017-12-06 18:04:10 +0100
commit7ced1ba0e6bf47efd75a4c7c607a99bc1198f4f3 (patch)
tree0dc68b5c4dc7053d112668bf2a48d09f8ca78ee5 /pretyping/patternops.ml
parent866b449c497933a3ab1185c194d8d33a86c432f2 (diff)
Getting rid of the Update constructor in Reductionops.
This was dead code, probably due to the fact it was once shared with the kernel stack type.
Diffstat (limited to 'pretyping/patternops.ml')
0 files changed, 0 insertions, 0 deletions