diff options
Diffstat (limited to 'plugins/decl_mode/decl_interp.ml')
| -rw-r--r-- | plugins/decl_mode/decl_interp.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/decl_mode/decl_interp.ml b/plugins/decl_mode/decl_interp.ml index 5e185f7e3..eb7d9e8e4 100644 --- a/plugins/decl_mode/decl_interp.ml +++ b/plugins/decl_mode/decl_interp.ml @@ -219,7 +219,7 @@ let interp_hyps_gen inject blend sigma env hyps head = let interp_hyps sigma env hyps = fst (interp_hyps_gen fst (fun x _ -> x) sigma env hyps glob_prop) -let dummy_prefix= id_of_string "__" +let dummy_prefix= Id.of_string "__" let rec deanonymize ids = function |