aboutsummaryrefslogtreecommitdiffhomepage
path: root/toplevel/command.ml
diff options
context:
space:
mode:
Diffstat (limited to 'toplevel/command.ml')
-rw-r--r--toplevel/command.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/toplevel/command.ml b/toplevel/command.ml
index 7c86d2d05..3995c4b1b 100644
--- a/toplevel/command.ml
+++ b/toplevel/command.ml
@@ -38,8 +38,8 @@ open Indschemes
open Misctypes
open Vernacexpr
-let do_universe l = Declare.do_universe l
-let do_constraint l = Declare.do_constraint l
+let do_universe poly l = Declare.do_universe poly l
+let do_constraint poly l = Declare.do_constraint poly l
let rec under_binders env sigma f n c =
if Int.equal n 0 then snd (f env sigma c) else