aboutsummaryrefslogtreecommitdiffhomepage
path: root/checker/term.mli
diff options
context:
space:
mode:
authorGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-06-08 17:37:25 +0200
committerGravatar Théo Zimmermann <theo.zimmermann@univ-paris-diderot.fr>2018-06-08 17:37:25 +0200
commitd063d30fea12141f84f3ff80608048e2903cbf6a (patch)
tree17daf16bf90d2ab533ac9a0e6d40aa1d82b2aa7b /checker/term.mli
parentbb63a9f2209108424bd3dadc1c479f9ddc0e1803 (diff)
parentafe5d78e85bc276a7a9b1386f504c98b02454463 (diff)
Merge PR #7747: dev/doc/univpoly.{txt => md}, split off primitive projection info
Diffstat (limited to 'checker/term.mli')
0 files changed, 0 insertions, 0 deletions