| NCic.Fixpoint _ -> []
| NCic.Inductive _ -> []
| NCic.Constant (_,_,_, ty, _) ->
- [ ty, NCic.Const(NReference.reference_of_spec
- uri (NReference.Def height)) ]
+ let ty = (* saturare *) ty in
+ [ty,NCic.Const(NReference.reference_of_spec uri (NReference.Def height))]
in
let status = basic_index_obj data status in
let dump = record_index_obj data :: status#dump in
(text,prefix_len,concl))
) seqs)
| GrafiteAst.NAuto (_loc, (l,a)) ->
- NTactics.auto_tac
+ NAuto.auto_tac
~params:(List.map (fun x -> "",0,x) l,a)
| GrafiteAst.NBranch _ -> NTactics.branch_tac
| GrafiteAst.NCases (_loc, what, where) ->
| 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