Permalink
Browse files

Renaming new_induct -> induction; new_destruct -> destruct.

  • Loading branch information...
1 parent 8bbd7ce commit f87c3a55b1ad52b63ebd0af0cf9f3fb0e8e86f76 @herbelin herbelin committed May 8, 2014
Showing with 23 additions and 21 deletions.
  1. +2 −0 dev/doc/changes.txt
  2. +2 −2 plugins/funind/indfun.ml
  3. +13 −13 tactics/tactics.ml
  4. +2 −2 tactics/tactics.mli
  5. +4 −4 toplevel/auto_ind_decl.ml
View
@@ -75,6 +75,8 @@
check_evars_are_solved explicitly to check that evars are solved.
See also the corresponding commit log.
+- Tactics API: new_induct -> induction; new_destruct -> destruct
+
=========================================
= CHANGES BETWEEN COQ V8.3 AND COQ V8.4 =
=========================================
View
@@ -26,8 +26,8 @@ let is_rec_info scheme_info =
let choose_dest_or_ind scheme_info =
if is_rec_info scheme_info
- then Tactics.new_induct false
- else Tactics.new_destruct false
+ then Tactics.induction false
+ else Tactics.destruct false
let functional_induction with_clean c princl pat =
Dumpglob.pause ();
View
@@ -3366,7 +3366,7 @@ let clear_unselected_context id inhyps cls gl =
thin ids gl
| None -> tclIDTAC gl
-let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
+let induction_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
let inhyps = match cls with
| Some {onhyps=Some hyps} -> List.map (fun ((_,id),_) -> id) hyps
| _ -> [] in
@@ -3404,8 +3404,8 @@ let new_induct_gen isrec with_evars elim (eqname,names) (sigma,(c,lbind)) cls =
atomic (using letins), then do induction. The specificity here is
that all arguments and parameters of the scheme are given
(mandatory for the moment), so we don't need to deal with
- parameters of the inductive type as in new_induct_gen. *)
-let new_induct_gen_l isrec with_evars elim (eqname,names) lc =
+ parameters of the inductive type as in induction_gen. *)
+let induction_gen_l isrec with_evars elim (eqname,names) lc =
if not (Option.is_empty eqname) then
errorlabstrm "" (str "Do not know what to do with " ++
Miscprint.pr_intro_pattern (Option.get eqname));
@@ -3451,14 +3451,14 @@ let new_induct_gen_l isrec with_evars elim (eqname,names) lc =
principles).
TODO: really unify induction with one and induction with several
args *)
-let induct_destruct isrec with_evars (lc,elim,names,cls) =
+let induction_destruct_core isrec with_evars (lc,elim,names,cls) =
assert (List.length lc > 0); (* ensured by syntax, but if called inside caml? *)
Proofview.Goal.raw_enter begin fun gl ->
let ifi = is_functional_induction elim gl in
if Int.equal (List.length lc) 1 && not ifi then
(* standard induction *)
onOpenInductionArg
- (fun c -> new_induct_gen isrec with_evars elim names c cls)
+ (fun c -> induction_gen isrec with_evars elim names c cls)
(List.hd lc)
else begin
(* functional induction *)
@@ -3481,36 +3481,36 @@ let induct_destruct isrec with_evars (lc,elim,names,cls) =
(fun (c,lbind) ->
if lbind != NoBindings then
error "'with' clause not supported here.";
- new_induct_gen_l isrec with_evars elim names [c]) (List.hd lc)
+ induction_gen_l isrec with_evars elim names [c]) (List.hd lc)
| _ ->
let newlc =
List.map (fun x ->
match x with (* FIXME: should we deal with ElimOnIdent? *)
| ElimOnConstr (x,NoBindings) -> x
| _ -> error "Don't know where to find some argument.")
lc in
- new_induct_gen_l isrec with_evars elim names newlc
+ induction_gen_l isrec with_evars elim names newlc
end
end
end
let induction_destruct isrec with_evars = function
| [],_,_ -> Proofview.tclUNIT ()
- | [a,b],el,cl -> induct_destruct isrec with_evars ([a],el,b,cl)
+ | [a,b],el,cl -> induction_destruct_core isrec with_evars ([a],el,b,cl)
| (a,b)::l,None,cl ->
Tacticals.New.tclTHEN
- (induct_destruct isrec with_evars ([a],None,b,cl))
- (Tacticals.New.tclMAP (fun (a,b) -> induct_destruct false with_evars ([a],None,b,cl)) l)
+ (induction_destruct_core isrec with_evars ([a],None,b,cl))
+ (Tacticals.New.tclMAP (fun (a,b) -> induction_destruct_core false with_evars ([a],None,b,cl)) l)
| l,Some el,cl ->
let check_basic_using = function
| a,(None,None) -> a
| _ -> error "Unsupported syntax for \"using\"."
in
let l' = List.map check_basic_using l in
- induct_destruct isrec with_evars (l', Some el, (None,None), cl)
+ induction_destruct_core isrec with_evars (l', Some el, (None,None), cl)
-let new_induct ev lc e idl cls = induct_destruct true ev (lc,e,idl,cls)
-let new_destruct ev lc e idl cls = induct_destruct false ev (lc,e,idl,cls)
+let induction ev lc e idl cls = induction_destruct_core true ev (lc,e,idl,cls)
+let destruct ev lc e idl cls = induction_destruct_core false ev (lc,e,idl,cls)
(* The registered tactic, which calls the default elimination
* if no elimination constant is provided. *)
View
@@ -266,7 +266,7 @@ val elim :
val simple_induct : quantified_hypothesis -> unit Proofview.tactic
-val new_induct : evars_flag ->
+val induction : evars_flag ->
(evar_map * constr with_bindings) induction_arg list ->
constr with_bindings option ->
intro_pattern_expr located option * intro_pattern_expr located option ->
@@ -278,7 +278,7 @@ val general_case_analysis : evars_flag -> constr with_bindings -> unit Proofvie
val simplest_case : constr -> unit Proofview.tactic
val simple_destruct : quantified_hypothesis -> unit Proofview.tactic
-val new_destruct : evars_flag ->
+val destruct : evars_flag ->
(evar_map * constr with_bindings) induction_arg list ->
constr with_bindings option ->
intro_pattern_expr located option * intro_pattern_expr located option ->
@@ -78,12 +78,12 @@ let sumbool = Coqlib.build_coq_sumbool
let andb = fun _ -> (Coqlib.build_bool_type()).Coqlib.andb
let induct_on c =
- new_induct false
+ induction false
[Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
None (None,None) None
let destruct_on_using c id =
- new_destruct false
+ destruct false
[Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
None
(None,Some (dl,IntroOrAndPattern [
@@ -92,7 +92,7 @@ let destruct_on_using c id =
None
let destruct_on c =
- new_destruct false
+ destruct false
[Tacexpr.ElimOnConstr (Evd.empty,(c,NoBindings))]
None (None,None) None
@@ -592,7 +592,7 @@ repeat ( apply andb_prop in z;let z1:= fresh "Z" in destruct z as [z1 z]).
apply_in false false freshz [Loc.ghost, (andb_prop(), NoBindings)] None;
Proofview.Goal.enter begin fun gl ->
let fresht = fresh_id (Id.of_string "Z") gl in
- (new_destruct false [Tacexpr.ElimOnConstr
+ (destruct false [Tacexpr.ElimOnConstr
(Evd.empty,((mkVar freshz,NoBindings)))]
None
(None, Some (dl,IntroOrAndPattern [[

0 comments on commit f87c3a5

Please sign in to comment.