match kind with
| NCic.Fixpoint _ -> []
| NCic.Inductive _ -> []
- | NCic.Constant (_,_,_, ty, _) ->
- [ ty, NCic.Const(NReference.reference_of_spec
- uri (NReference.Def height)) ]
+ | NCic.Constant (_,_,Some _, ty, _) ->
+ let ty,_,_ = NCicMetaSubst.saturate [] [] [] ty 0 in
+ [ty,NCic.Const(NReference.reference_of_spec uri (NReference.Def height))]
+ | NCic.Constant (_,_,None _, ty, _) ->
+ let ty,_,_ = NCicMetaSubst.saturate [] [] [] ty 0 in
+ [ty,NCic.Const(NReference.reference_of_spec uri (NReference.Decl))]
in
let status = basic_index_obj data status in
let dump = record_index_obj data :: status#dump in
| NCicTypeChecker.TypeCheckerFailure _ ->
HLog.warn "error in generating projection/eliminator";
status,uris
- ) (status,`New [] (* uris *)) boxml in
+ ) (status,`New [] (* uris *)) boxml in
+ let _,_,_,_,nobj = obj in
+ let status = match nobj with
+ NCic.Inductive (true,leftno,[it],_) ->
+ let _,ind_name,ty,cl = it in
+ List.fold_left
+ (fun status outsort ->
+ let status = status#set_ng_mode `ProofMode in
+ try
+ (let status,invobj = NInversion.mk_inverter
+ (ind_name ^ "_inv_" ^ (snd (NCicElim.ast_of_sort outsort)))
+ it leftno outsort status status#baseuri in
+ let _,_,menv,_,_ = invobj in
+ fst (match menv with
+ [] -> eval_ncommand opts status ("",0,GrafiteAst.NQed Stdpp.dummy_loc)
+ | _ -> status,`New []))
+ with _ -> HLog.warn "error in generating inversion principle";
+ let status = status#set_ng_mode `CommandMode in status)
+ status
+ (NCic.Prop::
+ List.map (fun s -> NCic.Type s) (NCicEnvironment.get_universes ()))
+ | _ -> status
+ in
let coercions =
match obj with
_,_,_,_,NCic.Inductive