diff options
Diffstat (limited to 'plugins/syntax/numeral.ml')
| -rw-r--r-- | plugins/syntax/numeral.ml | 15 |
1 files changed, 8 insertions, 7 deletions
diff --git a/plugins/syntax/numeral.ml b/plugins/syntax/numeral.ml index ec8c2338fb..9808c61255 100644 --- a/plugins/syntax/numeral.ml +++ b/plugins/syntax/numeral.ml @@ -1,6 +1,6 @@ (************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) -(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2019 *) (* <O___,, * (see CREDITS file for the list of authors) *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) @@ -12,7 +12,6 @@ open Pp open Util open Names open Libnames -open Globnames open Constrexpr open Constrexpr_ops open Notation @@ -31,7 +30,7 @@ let get_constructors ind = let mib,oib = Global.lookup_inductive ind in let mc = oib.Declarations.mind_consnames in Array.to_list - (Array.mapi (fun j c -> ConstructRef (ind, j + 1)) mc) + (Array.mapi (fun j c -> GlobRef.ConstructRef (ind, j + 1)) mc) let qualid_of_ref n = n |> Coqlib.lib_ref |> Nametab.shortest_qualid_of_global Id.Set.empty @@ -40,7 +39,7 @@ let q_option () = qualid_of_ref "core.option.type" let unsafe_locate_ind q = match Nametab.locate q with - | IndRef i -> i + | GlobRef.IndRef i -> i | _ -> raise Not_found let locate_z () = @@ -101,7 +100,9 @@ let type_error_of g ty = str " to Decimal.int or (option Decimal.int)." ++ fnl () ++ str "Instead of Decimal.int, the types Decimal.uint or Z or Int63.int or Decimal.decimal could be used (you may need to require BinNums or Decimal or Int63 first).") -let vernac_numeral_notation env sigma local ty f g scope opts = +let vernac_numeral_notation local ty f g scope opts = + let env = Global.env () in + let sigma = Evd.from_env env in let dec_ty = locate_decimal () in let z_pos_ty = locate_z () in let int63_ty = locate_int63 () in @@ -111,7 +112,7 @@ let vernac_numeral_notation env sigma local ty f g scope opts = let cty = mkRefC ty in let app x y = mkAppC (x,[y]) in let arrow x y = - mkProdC ([CAst.make Anonymous],Default Decl_kinds.Explicit, x, y) + mkProdC ([CAst.make Anonymous],Default Glob_term.Explicit, x, y) in let opt r = app (mkRefC (q_option ())) r in let constructors = get_constructors tyc in @@ -164,7 +165,7 @@ let vernac_numeral_notation env sigma local ty f g scope opts = { pt_local = local; pt_scope = scope; pt_interp_info = NumeralNotation o; - pt_required = Nametab.path_of_global (IndRef tyc),[]; + pt_required = Nametab.path_of_global (GlobRef.IndRef tyc),[]; pt_refs = constructors; pt_in_match = true } in |