aboutsummaryrefslogtreecommitdiffhomepage
path: root/kernel/kernel.mllib
diff options
context:
space:
mode:
authorGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-29 14:30:33 +0200
committerGravatar Maxime Dénès <mail@maximedenes.fr>2018-06-29 14:30:33 +0200
commit2ca003899ea4a24a470c32dc186b95ef3de3ca19 (patch)
treee7444295b47223d16db6db5beafde4839a0cf926 /kernel/kernel.mllib
parentacbc42ad1da48be53456c0d41ec2e60ae2d6e642 (diff)
parent21ed95122a088cab6808200778719270d9cc9078 (diff)
Merge PR #7080: Swapping Context and Constr and defining declarations on constr in Constr
Diffstat (limited to 'kernel/kernel.mllib')
-rw-r--r--kernel/kernel.mllib2
1 files changed, 1 insertions, 1 deletions
diff --git a/kernel/kernel.mllib b/kernel/kernel.mllib
index 50713b957..07a02f6ef 100644
--- a/kernel/kernel.mllib
+++ b/kernel/kernel.mllib
@@ -5,8 +5,8 @@ UGraph
Esubst
Sorts
Evar
-Constr
Context
+Constr
Vars
Term
Mod_subst