diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/tac2core.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/tac2core.ml b/src/tac2core.ml index 196755346d..b38f0b8582 100644 --- a/src/tac2core.ml +++ b/src/tac2core.ml @@ -21,6 +21,7 @@ open Proofview.Notations module Value = Tac2ffi +let std_core n = KerName.make2 Tac2env.std_prefix (Label.of_id (Id.of_string_soft n)) let coq_core n = KerName.make2 Tac2env.coq_prefix (Label.of_id (Id.of_string_soft n)) module Core = @@ -35,6 +36,7 @@ let t_constr = coq_core "constr" let t_pattern = coq_core "pattern" let t_ident = coq_core "ident" let t_option = coq_core "option" +let t_reference = std_core "reference" let c_nil = coq_core "[]" let c_cons = coq_core "::" @@ -730,7 +732,7 @@ let () = let () = let interp _ gr = return (Value.of_reference gr) in let obj = { - ml_type = t_pattern; + ml_type = t_reference; ml_interp = interp; } in define_ml_object Tac2env.wit_reference obj |