diff options
Diffstat (limited to 'library')
| -rw-r--r-- | library/declare.ml | 23 | ||||
| -rw-r--r-- | library/declare.mli | 4 |
2 files changed, 15 insertions, 12 deletions
diff --git a/library/declare.ml b/library/declare.ml index 31749152c0..5508432679 100644 --- a/library/declare.ml +++ b/library/declare.ml @@ -1,6 +1,7 @@ (* $Id$ *) +open Pp open Util open Names open Generic @@ -171,7 +172,8 @@ let declare_mind mie = | (id,_,_,_)::_ -> id | [] -> anomaly "cannot declare an empty list of inductives" in - let _ = add_leaf id CCI (in_inductive mie) in () + let sp = add_leaf id CCI (in_inductive mie) in + sp (* Test and access functions. *) @@ -280,19 +282,20 @@ let mind_path = function (* Eliminations. *) -let declare_eliminations sp = - let env = Global.env () in - let sigma = Evd.empty in - let mindid = basename sp in - let mind = global_reference (kind_of_path sp) mindid in - let redmind = minductype_spec env sigma mind in - let mindstr = string_of_id mindid in +let declare_eliminations sp i = + let oper = MutInd (sp,i) in + let ids = ids_of_sign (Global.var_context()) in + let mind = DOPN(oper, Array.of_list (List.map (fun id -> VAR id) ids)) in + let mispec = Global.lookup_mind_specif mind in + let mindstr = string_of_id (mis_typename mispec) in let declare na c = declare_constant (id_of_string na) ({ const_entry_body = c; const_entry_type = None }, - NeverDischarge,false) + NeverDischarge, false); + pPNL [< 'sTR na; 'sTR " is defined" >] in - let mispec = Global.lookup_mind_specif redmind in + let env = Global.env () in + let sigma = Evd.empty in let elim_scheme = strip_all_casts (mis_make_indrec env sigma [] mispec).(0) in let npars = mis_nparams mispec in diff --git a/library/declare.mli b/library/declare.mli index 4fe7767fd6..f5c2dff07c 100644 --- a/library/declare.mli +++ b/library/declare.mli @@ -28,9 +28,9 @@ val declare_constant : identifier -> constant_declaration -> unit val declare_parameter : identifier -> constr -> unit -val declare_mind : mutual_inductive_entry -> unit +val declare_mind : mutual_inductive_entry -> section_path -val declare_eliminations : section_path -> unit +val declare_eliminations : section_path -> int -> unit val make_strength : string list -> strength val make_strength_0 : unit -> strength |