aboutsummaryrefslogtreecommitdiffhomepage
path: root/pretyping/unification.ml
diff options
context:
space:
mode:
authorGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-02-21 15:47:51 +0100
committerGravatar Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net>2018-03-09 16:30:11 +0100
commitee7f5486fff86c453767997f97eda381983c4bbc (patch)
tree327e64c5324962e40c58e6a012b19b84d4955c66 /pretyping/unification.ml
parentdb0918bfa5089f9ab44374504cbd0ddc758ea1e5 (diff)
Option for messing with inference of irrelevant constraints
Diffstat (limited to 'pretyping/unification.ml')
0 files changed, 0 insertions, 0 deletions