diff options
Diffstat (limited to 'plugins/extraction/table.ml')
| -rw-r--r-- | plugins/extraction/table.ml | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/plugins/extraction/table.ml b/plugins/extraction/table.ml index 607ca1b3a9..ca98f07e8d 100644 --- a/plugins/extraction/table.ml +++ b/plugins/extraction/table.ml @@ -1,16 +1,15 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open API open Names +open ModPath open Term open Declarations -open Nameops open Namegen open Libobject open Goptions @@ -36,14 +35,14 @@ module Refset' = Refset_env let occur_kn_in_ref kn = function | IndRef (kn',_) - | ConstructRef ((kn',_),_) -> Names.eq_mind kn kn' + | ConstructRef ((kn',_),_) -> MutInd.equal kn kn' | ConstRef _ -> false | VarRef _ -> assert false let repr_of_r = function - | ConstRef kn -> repr_con kn + | ConstRef kn -> Constant.repr3 kn | IndRef (kn,_) - | ConstructRef ((kn,_),_) -> repr_mind kn + | ConstructRef ((kn,_),_) -> MutInd.repr3 kn | VarRef _ -> assert false let modpath_of_r r = @@ -65,7 +64,7 @@ let raw_string_of_modfile = function | _ -> assert false let is_toplevel mp = - ModPath.equal mp initial_path || ModPath.equal mp (Lib.current_mp ()) + ModPath.equal mp ModPath.initial || ModPath.equal mp (Lib.current_mp ()) let at_toplevel mp = is_modfile mp || is_toplevel mp @@ -265,8 +264,8 @@ let safe_basename_of_global r = anomaly (Pp.str "Inductive object unknown to extraction and not globally visible.") in match r with - | ConstRef kn -> Label.to_id (con_label kn) - | IndRef (kn,0) -> Label.to_id (mind_label kn) + | ConstRef kn -> Label.to_id (Constant.label kn) + | IndRef (kn,0) -> Label.to_id (MutInd.label kn) | IndRef (kn,i) -> (try (unsafe_lookup_ind kn).ind_packets.(i).ip_typename with Not_found -> last_chance r) @@ -287,8 +286,8 @@ let safe_pr_long_global r = try Printer.pr_global r with Not_found -> match r with | ConstRef kn -> - let mp,_,l = repr_con kn in - str ((string_of_mp mp)^"."^(Label.to_string l)) + let mp,_,l = Constant.repr3 kn in + str ((ModPath.to_string mp)^"."^(Label.to_string l)) | _ -> assert false let pr_long_mp mp = @@ -417,7 +416,7 @@ let error_singleton_become_prop id og = str " (or in its mutual block)" | None -> mt () in - err (str "The informative inductive type " ++ pr_id id ++ + err (str "The informative inductive type " ++ Id.print id ++ str " has a Prop instance" ++ loc ++ str "." ++ fnl () ++ str "This happens when a sort-polymorphic singleton inductive type\n" ++ str "has logical parameters, such as (I,I) : (True * True) : Prop.\n" ++ @@ -445,9 +444,10 @@ let error_MPfile_as_mod mp b = "Please "^s2^"use (Recursive) Extraction Library instead.\n")) let argnames_of_global r = - let typ = Global.type_of_global_unsafe r in + let env = Global.env () in + let typ, _ = Global.type_of_global_in_context env r in let rels,_ = - decompose_prod (Reduction.whd_all (Global.env ()) typ) in + decompose_prod (Reduction.whd_all env typ) in List.rev_map fst rels let msg_of_implicit = function @@ -722,7 +722,7 @@ let add_implicits r l = let i = List.index Name.equal (Name id) names in Int.Set.add i s with Not_found -> - err (str "No argument " ++ pr_id id ++ str " for " ++ + err (str "No argument " ++ Id.print id ++ str " for " ++ safe_pr_global r) in let ints = List.fold_left add_arg Int.Set.empty l in @@ -800,7 +800,7 @@ let extraction_blacklist l = (* Printing part *) let print_extraction_blacklist () = - prlist_with_sep fnl pr_id (Id.Set.elements !blacklist_table) + prlist_with_sep fnl Id.print (Id.Set.elements !blacklist_table) (* Reset part *) @@ -878,7 +878,7 @@ let extract_constant_inline inline r ids s = match g with | ConstRef kn -> let env = Global.env () in - let typ = Global.type_of_global_unsafe (ConstRef kn) in + let typ, _ = Global.type_of_global_in_context env (ConstRef kn) in let typ = Reduction.whd_all env typ in if Reduction.is_arity env typ then begin |