let rec mk_arrows ~jmeq xs ys selection target =
match selection,xs,ys with
[],[],[] -> target
- | false :: l,x::xs,y::ys -> mk_arrows ~jmeq xs ys l target
+ | false :: l,_x::xs,_y::ys -> mk_arrows ~jmeq xs ys l target
| true :: l,x::xs,y::ys when jmeq ->
NotationPt.Binder (`Forall, (mk_id "_",
Some (mk_appl [mk_sym "jmsimeq" ;
status#set_obj(u,h,NCicUntrusted.apply_subst_metasenv status subst metasenv,subst,o)
;;
-let mk_inverter ~jmeq name is_ind it leftno ?selection outsort (status: #NCic.status) baseuri =
+let mk_inverter ~jmeq name _is_ind it leftno ?selection outsort (status: #NCic.status) baseuri =
pp (lazy ("leftno = " ^ string_of_int leftno));
let _,ind_name,ty,cl = it in
pp (lazy ("arity: " ^ status#ppterm ~metasenv:[] ~subst:[] ~context:[] ty));
let nparams = List.length args in
(* the default is a dependent inversion *)
- let is_dependent = (selection = None && jmeq) in
+ let is_dependent = (selection = None && (jmeq || nparams = 0)) in
pp (lazy ("nparams = " ^ string_of_int nparams));
- if nparams = 0
+ if (nparams = 0 && not is_dependent)
then raise (Failure "inverter: the type must have at least one right parameter")
else
let xs = List.map (fun n -> "x" ^ (string_of_int n)) (HExtlib.list_seq 1 (leftno+nparams+1)) in
in (hypaux 1 ncons)
in
- let outsort, suffix = NCicElim.ast_of_sort outsort in
+ let outsort, _suffix = NCicElim.ast_of_sort outsort in
let theorem =
mk_prods xs
(NotationPt.Binder (`Forall, (mk_id "Hterm", Some (mk_appl (List.map mk_id (ind_name::xs)))),
mk_prods hyplist (mk_appl (mk_id "P"::id_rs))))))
in
let status, theorem =
- GrafiteDisambiguate.disambiguate_nobj status ~baseuri
+ let attrs = `Generated, `Theorem, `InversionPrinciple in
+ GrafiteDisambiguate.disambiguate_nobj status ~baseuri
(baseuri ^ name ^ ".def",0,
NotationPt.Theorem
- (`Theorem,name,theorem,
- Some (NotationPt.Implicit (`Tagged "inv")),`InversionPrinciple))
+ (name,theorem, Some (NotationPt.Implicit (`Tagged "inv")), attrs))
in
- let uri,height,nmenv,nsubst,nobj = theorem in
+ let _uri,_height,nmenv,_nsubst,_nobj = theorem in
let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
let status = status#set_obj theorem in
let status = status#set_stack ninitial_stack in
"",0,(None,[],
Some (if jmeq then jmeqpatt selection
else leibpatt selection)) in
- let elim_tac = if is_ind then NTactics.elim_tac else NTactics.cases_tac in
+ (* let elim_tac = if is_ind then NTactics.elim_tac else NTactics.cases_tac in *)
+ let elim_tac ~what ~where s =
+ try NTactics.elim_tac ~what ~where s
+ with NTacStatus.Error _ -> NTactics.cases_tac ~what ~where s
+ in
let status =
NTactics.block_tac
(NTactics.branch_tac ::
let mk_inverter name is_ind it leftno ?selection outsort status baseuri =
try mk_inverter ~jmeq:true name is_ind it leftno ?selection outsort status baseuri
- with NTacStatus.Error (s,_) ->
+ with NTacStatus.Error (_s,_) ->
mk_inverter ~jmeq:false name is_ind it leftno ?selection outsort status baseuri
;;