aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--interp/constrarg.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index cb980f5a38..aad034c055 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -67,5 +67,5 @@ let () =
register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern";
register_name0 wit_tactic "Constrarg.wit_tactic";
register_name0 wit_sort "Constrarg.wit_sort";
- register_name0 wit_uconstr "Constrarg.uconstr";
+ register_name0 wit_uconstr "Constrarg.wit_uconstr";
register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl";