aboutsummaryrefslogtreecommitdiffhomepage
path: root/interp/constrarg.ml
diff options
context:
space:
mode:
Diffstat (limited to 'interp/constrarg.ml')
-rw-r--r--interp/constrarg.ml21
1 files changed, 0 insertions, 21 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 20ee7aa4f..81e942d82 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -63,27 +63,6 @@ let wit_red_expr = Genarg.make0 "redexpr"
let wit_clause_dft_concl =
Genarg.make0 "clause_dft_concl"
-(** Register location *)
-
-let () =
- register_name0 wit_int_or_var "Constrarg.wit_int_or_var";
- register_name0 wit_ref "Constrarg.wit_ref";
- register_name0 wit_ident "Constrarg.wit_ident";
- register_name0 wit_var "Constrarg.wit_var";
- 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_constr "Constrarg.wit_constr";
- register_name0 wit_uconstr "Constrarg.wit_uconstr";
- register_name0 wit_open_constr "Constrarg.wit_open_constr";
- register_name0 wit_constr_may_eval "Constrarg.wit_constr_may_eval";
- register_name0 wit_red_expr "Constrarg.wit_red_expr";
- register_name0 wit_clause_dft_concl "Constrarg.wit_clause_dft_concl";
- register_name0 wit_quant_hyp "Constrarg.wit_quant_hyp";
- register_name0 wit_bindings "Constrarg.wit_bindings";
- register_name0 wit_constr_with_bindings "Constrarg.wit_constr_with_bindings";
- ()
-
(** Aliases *)
let wit_reference = wit_ref