- let _,indname,_,cl = it in
+ let _,_indname,_,cl = it in
let _,_,t_k = List.nth cl consno in
List.length (arg_list nleft t_k) ;;
let _,_,t_k = List.nth cl consno in
List.length (arg_list nleft t_k) ;;
(* creates the discrimination = injection+contradiction principle *)
exception ConstructorTooBig of string;;
(* creates the discrimination = injection+contradiction principle *)
exception ConstructorTooBig of string;;
- (`Theorem,name,principle,
- Some (NotationPt.Implicit (`Tagged "inv")),`DiscriminationPrinciple))
+ (name, principle, Some (NotationPt.Implicit (`Tagged "inv")), attrs))
- 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
let status = subst_metasenv_and_fix_names status in
(* PHASE 3: we finally prove the discrimination principle *)
let ninitial_stack = Continuationals.Stack.of_nmetasenv nmenv in
let status = status#set_obj theorem in
let status = status#set_stack ninitial_stack in
let status = subst_metasenv_and_fix_names status in
(* PHASE 3: we finally prove the discrimination principle *)
let refl_id = mk_sym "refl" in
pp (lazy (Printf.sprintf "dbranch %d %d" leftno consno));
let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in
let refl_id = mk_sym "refl" in
pp (lazy (Printf.sprintf "dbranch %d %d" leftno consno));
let nlist = HExtlib.list_seq 0 (nargs it leftno consno) in
| NCic.Rel var ->
cascade_select_in_ctx status ~subst:(get_subst status) context skip (var+cur_eq)
| _ -> cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in
| NCic.Rel var ->
cascade_select_in_ctx status ~subst:(get_subst status) context skip (var+cur_eq)
| _ -> cascade_select_in_ctx status ~subst:(get_subst status) context skip cur_eq in
let names_to_gen = List.filter (fun n -> n <> eq_name) names_to_gen in
if (List.exists (fun x -> List.mem x skip) names_to_gen)
then oldstatus
else
let gen_tac x =
(fun s ->
let names_to_gen = List.filter (fun n -> n <> eq_name) names_to_gen in
if (List.exists (fun x -> List.mem x skip) names_to_gen)
then oldstatus
else
let gen_tac x =
(fun s ->
~what:("",0,mk_id eq_name) ~where:default_pattern;
(* NTactics.reduce_tac ~reduction:(`Normalize true)
~where:default_pattern;*)
~what:("",0,mk_id eq_name) ~where:default_pattern;
(* NTactics.reduce_tac ~reduction:(`Normalize true)
~where:default_pattern;*)
status, Some (List.length ctx - i), kind
| `Cycle | `Blob | `NonEq -> aux (i+1) (* XXX: skip cyclic/blob equations for now *)
| _ ->
status, Some (List.length ctx - i), kind
| `Cycle | `Blob | `NonEq -> aux (i+1) (* XXX: skip cyclic/blob equations for now *)
| _ ->
let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
let acc = rm_eq has_cleared acc in
let skip = rm_eq has_cleared skip in
let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
let acc = rm_eq has_cleared acc in
let skip = rm_eq has_cleared skip in
let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
let acc = rm_eq has_cleared acc in
let skip = rm_eq has_cleared skip in
let rm_eq b l = if b then List.filter (fun x -> x <> eq_name) l else l in
let acc = rm_eq has_cleared acc in
let skip = rm_eq has_cleared skip in