aboutsummaryrefslogtreecommitdiff
path: root/interp
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2013-12-01 18:47:55 +0100
committerPierre-Marie Pédrot2013-12-01 18:55:11 +0100
commitcb290d81c46ec370e303e1414e203c40c8fa1174 (patch)
tree8f48d26fe7f68a905c2194239523c91316dc0139 /interp
parent233a782a2336f003869f82e697a567ed02885f23 (diff)
Removing RefArgType generic argument.
Diffstat (limited to 'interp')
-rw-r--r--interp/constrarg.ml3
1 files changed, 2 insertions, 1 deletions
diff --git a/interp/constrarg.ml b/interp/constrarg.ml
index 97004a93dd..4f20dd5606 100644
--- a/interp/constrarg.ml
+++ b/interp/constrarg.ml
@@ -47,7 +47,7 @@ let wit_pattern_ident = wit_ident_gen false
let wit_var = unsafe_of_type VarArgType
-let wit_ref = unsafe_of_type RefArgType
+let wit_ref = Genarg.make0 None "ref"
let wit_quant_hyp = unsafe_of_type QuantHypArgType
@@ -71,6 +71,7 @@ let wit_red_expr = unsafe_of_type RedExprArgType
(** Register location *)
let () =
+ register_name0 wit_ref "Constrarg.wit_ref";
register_name0 wit_intro_pattern "Constrarg.wit_intro_pattern";
register_name0 wit_tactic "Constrarg.wit_tactic";
register_name0 wit_sort "Constrarg.wit_sort";