diff options
Diffstat (limited to 'toplevel/ind_tables.ml')
| -rw-r--r-- | toplevel/ind_tables.ml | 34 |
1 files changed, 20 insertions, 14 deletions
diff --git a/toplevel/ind_tables.ml b/toplevel/ind_tables.ml index 53c3bcea..77cfa6fa 100644 --- a/toplevel/ind_tables.ml +++ b/toplevel/ind_tables.ml @@ -1,13 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -(*i $Id: ind_tables.ml 14641 2011-11-06 11:59:10Z herbelin $ i*) - (* File created by Vincent Siles, Oct 2007, extended into a generic support for generation of inductive schemes by Hugo Herbelin, Nov 2009 *) @@ -53,7 +51,7 @@ let discharge_scheme (_,(kind,l)) = Some (kind,Array.map (fun (ind,const) -> (Lib.discharge_inductive ind,Lib.discharge_con const)) l) -let (inScheme,_) = +let inScheme : string * (inductive * constant) array -> obj = declare_object {(default_object "SCHEME") with cache_function = cache_scheme; load_function = (fun _ -> cache_scheme); @@ -88,8 +86,9 @@ let scheme_object_table = (Hashtbl.create 17 : (string, string * scheme_object_function) Hashtbl.t) let declare_scheme_object s aux f = - (try check_ident ("ind"^s) with _ -> - error ("Illegal induction scheme suffix: "^s)); + (try check_ident ("ind"^s) + with e when Errors.noncritical e -> + error ("Illegal induction scheme suffix: "^s)); let key = if aux = "" then s else aux in try let _ = Hashtbl.find scheme_object_table key in @@ -111,21 +110,28 @@ let declare_individual_scheme_object s ?(aux="") f = let declare_scheme kind indcl = Lib.add_anonymous_leaf (inScheme (kind,indcl)) +let is_visible_name id = + try ignore (Nametab.locate (Libnames.qualid_of_ident id)); true + with Not_found -> false + +let compute_name internal id = + match internal with + | KernelVerbose | UserVerbose -> id + | KernelSilent -> + Namegen.next_ident_away_from (add_prefix "internal_" id) is_visible_name + let define internal id c = - (* TODO: specify even more by distinguish between KernelVerbose and - * UserVerbose *) - let fd = match internal with - | KernelSilent -> declare_internal_constant - | _ -> declare_constant in + let fd = declare_constant ~internal in + let id = compute_name internal id in let kn = fd id (DefinitionEntry { const_entry_body = c; + const_entry_secctx = None; const_entry_type = None; - const_entry_opaque = false; - const_entry_boxed = Flags.boxed_definitions() }, + const_entry_opaque = false }, Decl_kinds.IsDefinition Scheme) in (match internal with - | KernelSilent -> () + | KernelSilent -> () | _-> definition_message id); kn |