aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--kernel/environ.ml3
-rw-r--r--kernel/environ.mli3
-rw-r--r--kernel/sign.ml1
-rw-r--r--kernel/sign.mli1
-rw-r--r--kernel/term.ml11
-rw-r--r--kernel/term.mli5
-rw-r--r--proofs/logic.ml16
-rw-r--r--proofs/proof_trees.ml13
-rw-r--r--tactics/tactics.ml168
9 files changed, 121 insertions, 100 deletions
diff --git a/kernel/environ.ml b/kernel/environ.ml
index 100db950f..0c6167a15 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -88,6 +88,9 @@ let fold_var_context f env a =
(fun d (env,e) -> (push_var d env, f env d e))
(var_context env) (reset_context env,a))
+let fold_var_context_reverse f a env =
+ Sign.fold_var_context_reverse f a (var_context env)
+
let process_var_context f env =
Sign.fold_var_context
(fun d env -> f env d) (var_context env) (reset_context env)
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 42d560ec9..dc733b3b4 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -56,6 +56,9 @@ val map_context : (constr -> constr) -> env -> env
val fold_var_context : (env -> var_declaration -> 'a -> 'a) -> env -> 'a -> 'a
val process_var_context : (env -> var_declaration -> env) -> env -> env
+(* Recurrence on [var_context] starting from younger decl *)
+val fold_var_context_reverse : ('a -> var_declaration -> 'a) -> 'a -> env -> 'a
+
(* [process_var_context_both_sides f env] iters [f] on the var
declarations of [env] taking as argument both the initial segment, the
middle value and the tail segment *)
diff --git a/kernel/sign.ml b/kernel/sign.ml
index 27aa150e6..d9438eb98 100644
--- a/kernel/sign.ml
+++ b/kernel/sign.ml
@@ -43,6 +43,7 @@ let rec mem_var_context id = function
| _ :: sign -> mem_var_context id sign
| [] -> false
let fold_var_context = List.fold_right
+let fold_var_context_reverse = List.fold_left
let fold_var_context_both_sides = list_fold_right_and_left
let it_var_context_quantifier f = List.fold_left (fun c d -> f d c)
diff --git a/kernel/sign.mli b/kernel/sign.mli
index bb2e083de..30e1dae28 100644
--- a/kernel/sign.mli
+++ b/kernel/sign.mli
@@ -25,6 +25,7 @@ val ids_of_var_context : var_context -> identifier list
val map_var_context : (constr -> constr) -> var_context -> var_context
val mem_var_context : identifier -> var_context -> bool
val fold_var_context : (var_declaration -> 'a -> 'a) -> var_context -> 'a -> 'a
+val fold_var_context_reverse : ('a -> var_declaration -> 'a) -> 'a -> var_context -> 'a
val fold_var_context_both_sides :
('a -> var_declaration -> var_context -> 'a) -> var_context -> 'a -> 'a
val it_var_context_quantifier :
diff --git a/kernel/term.ml b/kernel/term.ml
index 9829c1154..9e3ed3479 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -957,6 +957,12 @@ let substl laml =
substn_many (Array.map make_substituend (Array.of_list laml)) 0
let subst1 lam = substl [lam]
+let substl_decl laml (id,bodyopt,typ as d) =
+ match bodyopt with
+ | None -> (id,None,substl laml typ)
+ | Some body -> (id, Some (substl laml body), typed_app (substl laml) typ)
+let subst1_decl lam = substl_decl [lam]
+
(* (thin_val sigma) removes identity substitutions from sigma *)
let rec thin_val = function
@@ -1425,6 +1431,11 @@ let occur_var s c =
in
try occur_rec c; false with Occur -> true
+let occur_var_in_decl hyp (_,c,typ) =
+ match c with
+ | None -> occur_var hyp (body_of_type typ)
+ | Some body -> occur_var hyp (body_of_type typ) || occur_var hyp body
+
(***************************************)
(* alpha and eta conversion functions *)
(***************************************)
diff --git a/kernel/term.mli b/kernel/term.mli
index fe26462de..7bba6d924 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -478,6 +478,9 @@ val substnl : constr list -> int -> constr -> constr
val substl : constr list -> constr -> constr
val subst1 : constr -> constr -> constr
+val substl_decl : constr list -> var_declaration -> var_declaration
+val subst1_decl : constr -> var_declaration -> var_declaration
+
(* [global_vars c] returns the list of [id]'s occurring as [VAR id] in [c] *)
val global_vars : constr -> identifier list
@@ -526,6 +529,8 @@ val occur_evar : existential_key -> constr -> bool
in c, [false] otherwise *)
val occur_var : identifier -> constr -> bool
+val occur_var_in_decl : identifier -> var_declaration -> bool
+
(* [dependent M N] is true iff M is eq\_constr with a subterm of N
M is appropriately lifted through abstractions of N *)
val dependent : constr -> constr -> bool
diff --git a/proofs/logic.ml b/proofs/logic.ml
index 2487d9160..aebc76539 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -188,16 +188,11 @@ let split_sign hfrom hto l =
in
splitrec [] false l
-let occur_decl hyp (_,c,typ) =
- match c with
- | None -> occur_var hyp (body_of_type typ)
- | Some body -> occur_var hyp (body_of_type typ) || occur_var hyp body
-
let move_after with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto =
let test_dep (hyp,c,typ as d) (hyp2,c,typ2 as d2) =
if toleft
- then occur_decl hyp2 d
- else occur_decl hyp d2
+ then occur_var_in_decl hyp2 d
+ else occur_var_in_decl hyp d2
in
let rec moverec first middle = function
| [] -> error ("No such hypothesis : " ^ (string_of_id hto))
@@ -249,11 +244,8 @@ let check_backward_dependencies env d =
let check_forward_dependencies id tail =
List.iter
- (function (id',c,t) ->
- let b = match c with
- | None -> occur_var id (body_of_type t)
- | Some body -> occur_var id (body_of_type t) || occur_var id body in
- if b then
+ (function (id',_,_ as decl) ->
+ if occur_var_in_decl id decl then
error ((string_of_id id) ^ " is used in the hypothesis "
^ (string_of_id id')))
tail
diff --git a/proofs/proof_trees.ml b/proofs/proof_trees.ml
index 30e5aeba2..2f7d069a8 100644
--- a/proofs/proof_trees.ml
+++ b/proofs/proof_trees.ml
@@ -371,4 +371,15 @@ let ast_of_cvt_arg = function
| Cofixexp (id,c) -> ope ("COFIXEXP",[(nvar (string_of_id id));
(ope ("COMMAND",[c]))])
| Intropattern p -> ast_of_cvt_intro_pattern p
- | Letpatterns _ -> failwith "TODO: ast_of_cvt_arg: Letpatterns"
+ | Letpatterns (gl_occ_opt,hyp_occ_list) ->
+ let hyps_pats =
+ List.map
+ (fun (id,l) ->
+ ope ("HYPPATTERN", nvar (string_of_id id) :: (List.map num l)))
+ hyp_occ_list in
+ let all_pats =
+ match gl_occ_opt with
+ | None -> hyps_pats
+ | Some l -> hyps_pats @ [ope ("CCLPATTERN", List.map num l)] in
+ ope ("LETPATTERNS", all_pats)
+
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 0c8451870..7597d044e 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -277,7 +277,7 @@ type intro_name_flag =
| IBasedOn of identifier * identifier list
| IMustBe of identifier
-let rec central_intro name_flag move_flag force_flag gl =
+let rec intro_gen name_flag move_flag force_flag gl =
try
let id =
match name_flag with
@@ -298,19 +298,22 @@ let rec central_intro name_flag move_flag force_flag gl =
if force_flag then
try
((tclTHEN (reduce (Red true) [])
- (central_intro name_flag move_flag force_flag)) gl)
+ (intro_gen name_flag move_flag force_flag)) gl)
with Redelimination ->
errorlabstrm "Intro"
[<'sTR "No product even after head-reduction">]
else
raise e
-let intro_using_warning id = central_intro (IMustBe id) None false
-let intro_using id = central_intro (IBasedOn (id,[])) None false
-let intro_force force_flag = central_intro (IAvoid []) None force_flag
+let intro_using_warning id = intro_gen (IMustBe id) None false
+let intro_using id = intro_gen (IBasedOn (id,[])) None false
+let intro_force force_flag = intro_gen (IAvoid []) None force_flag
let intro = intro_force false
let introf = intro_force true
+(* For backwards compatibility *)
+let central_intro = intro_gen
+
(**** Multiple introduction tactics ****)
let rec intros_using = function
@@ -335,14 +338,14 @@ let intros_replacing ids gls =
(* User-level introduction tactics *)
let dyn_intro = function
- | [] -> central_intro (IAvoid []) None true
- | [Identifier id] -> central_intro (IMustBe id) None true
+ | [] -> intro_gen (IAvoid []) None true
+ | [Identifier id] -> intro_gen (IMustBe id) None true
| l -> bad_tactic_args "intro" l
let dyn_intro_move = function
- | [Identifier id2] -> central_intro (IAvoid []) (Some id2) true
+ | [Identifier id2] -> intro_gen (IAvoid []) (Some id2) true
| [Identifier id; Identifier id2] ->
- central_intro (IMustBe id) (Some id2) true
+ intro_gen (IMustBe id) (Some id2) true
| l -> bad_tactic_args "intro_move" l
let rec intros_until s g =
@@ -396,15 +399,10 @@ let intros_do n g =
let rec intros_move = function
| [] -> tclIDTAC
| (hyp,destopt) :: rest ->
- tclTHEN (central_intro (IMustBe hyp) destopt false)
+ tclTHEN (intro_gen (IMustBe hyp) destopt false)
(intros_move rest)
-let occur_var_in_decl id (c,t) =
- match c with
- | None -> occur_var id (body_of_type t)
- | Some body -> occur_var id body || occur_var id (body_of_type t)
-
-let dependent_in_decl a (c,t) =
+let dependent_in_decl a (_,c,t) =
match c with
| None -> dependent a (body_of_type t)
| Some body -> dependent a body || dependent a (body_of_type t)
@@ -419,13 +417,13 @@ let move_to_rhyp rhyp gl =
if Some hyp = rhyp then
lastfixed
else if List.exists (occur_var_in_decl hyp) depdecls then
- get_lhyp lastfixed ((c,typ)::depdecls) rest
+ get_lhyp lastfixed (ht::depdecls) rest
else
get_lhyp (Some hyp) depdecls rest
in
let sign = pf_hyps gl in
- let (hyp,c,typ) = List.hd sign in
- match get_lhyp None [c,typ] sign with
+ let (hyp,c,typ as decl) = List.hd sign in
+ match get_lhyp None [decl] sign with
| None -> tclIDTAC gl
| Some hypto -> move_hyp true hyp hypto gl
@@ -588,9 +586,9 @@ let generalize_goal gl c cl =
let generalize_dep c gl =
let sign = pf_hyps gl in
let init_ids = ids_of_var_context (Global.var_context()) in
- let rec seek toquant (h,body,t as d) =
- if List.exists (fun (id,_,_) -> occur_var_in_decl id (body,t)) toquant
- or dependent_in_decl c (body,t) then
+ let rec seek toquant d =
+ if List.exists (fun (id,_,_) -> occur_var_in_decl id d) toquant
+ or dependent_in_decl c d then
d::toquant
else
toquant
@@ -643,7 +641,7 @@ let quantify lconstr =
[letin_tac b na c occ_ccl occ_hyps gl] transforms
[...x1:T1(c),...,x2:T2(c),... |- G(c)] into
[...x:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is false or
- [...x:T;H:x=c;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is true
+ [...x:=c:T;x1:T1(x),...,x2:T2(x),... |- G(x)] if [b] is true
[occ_hyps] and [occ_ccl] tells which occurrences of [c] have to be substd;
if [occ_hyps] is empty, [c] is substituted in every hyp where it occurs;
@@ -654,14 +652,14 @@ let quantify lconstr =
used to remember the place of x1, x2, ...: it is the list of hypotheses on
the left of each x1, ...).
*)
-(*
+
let letin_abstract id c occ_ccl occ_hyps gl =
let allhyp = occ_hyps=[] in
- let hyps = pf_hyps gl in
+ let env = pf_env gl in
let abstract ((depdecls,marks,occl as accu),lhyp) (hyp,bodyopt,typ as d) =
try
let occ = if allhyp then [] else List.assoc hyp occl in
- let newdecl = subst1 (mkVar id) (subst_term_occ_decl occ c d) in
+ let newdecl = subst1_decl (mkVar id) (subst_term_occ_decl occ c d) in
let newoccl = list_except_assoc hyp occl in
if d=newdecl then
(accu,Some hyp)
@@ -671,10 +669,10 @@ let letin_abstract id c occ_ccl occ_hyps gl =
(accu,Some hyp)
in
let (depdecls,marks,rest),_ =
- it_sign abstract (([],[],[],occ_hyps),None) hyps in
+ fold_var_context_reverse abstract (([],[],occ_hyps),None) env in
if rest <> [] then begin
let id = fst (List.hd rest) in
- if mem_sign hyps id
+ if mem_var_context id (var_context env)
then error ("Hypothesis "^(string_of_id id)^" occurs twice")
else error ("No such hypothesis : " ^ (string_of_id id))
end;
@@ -686,9 +684,11 @@ let letin_abstract id c occ_ccl occ_hyps gl =
let letin_tac with_eq name c occ_ccl occ_hyps gl =
let x = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c) name in
- let hyps = pf_untyped_hyps gl in
- let id = next_global_ident_away x (ids_of_sign hyps) in
- if mem_sign hyps id then error "New variable is already declared";
+ let env = pf_env gl in
+ let used_ids = ids_of_context env in
+ let id = next_global_ident_away x used_ids in
+ if mem_var_context id (var_context env) then
+ error "New variable is already declared";
let (depdecls,marks,ccl)= letin_abstract id c occ_ccl occ_hyps gl in
let t = pf_type_of gl c in
let (eqc,reflc) =
@@ -699,23 +699,23 @@ let letin_tac with_eq name c occ_ccl occ_hyps gl =
(pf_parse_const gl "eqT", pf_parse_const gl "refl_eqT")
else error "Not possible with proofs yet"
in
- let heq = next_global_ident_away (id_of_string "Heq") (ids_of_sign hyps) in
+ let heq = next_global_ident_away (id_of_string "Heq") used_ids in
let tmpcl = List.fold_right mkNamedProd_or_LetIn depdecls ccl in
- let tmpargs = List.map (fun (id,_,_) -> mkVar id) depdecls in
- let newcl,args =
+ let args = List.map (fun (id,_,_) -> mkVar id) depdecls in
+ let newcl =
if with_eq then
let eq = applist (eqc,[t;mkVar id;c]) in
let refl = applist (reflc,[t;c]) in
- (mkNamedProd id t (mkNamedProd heq eq tmpcl), c::refl::tmpargs)
+ mkNamedLetIn id c t tmpcl
else
- (mkNamedProd id t tmpcl, c::tmpargs)
+ mkNamedProd id t tmpcl
in
let lastlhyp = if marks=[] then None else snd (List.hd marks) in
tclTHENLIST
[ apply_type newcl args;
- thin dephyps;
- central_intro (IMustBe id) lastlhyp false;
- if with_eq then central_intro (IMustBe heq) lastlhyp false else tclIDTAC;
+ thin (List.map (fun (id,_,_) -> id) depdecls);
+ intro_gen (IMustBe id) lastlhyp false;
+(* if with_eq then intro_gen (IMustBe heq) lastlhyp false else tclIDTAC;*)
intros_move marks ] gl
let dyn_lettac args gl = match args with
@@ -724,8 +724,6 @@ let dyn_lettac args gl = match args with
| [Identifier id; Constr c; Letpatterns (o,l)] ->
letin_tac true (Name id) c o l gl
| l -> bad_tactic_args "letin" l
-*)
-let dyn_lettac a = failwith "TO REDO"
(********************************************************************)
(* Exact tactics *)
@@ -1053,13 +1051,13 @@ let induct_discharge indpath statuslists cname destopt avoid (_,t) =
| IsProd (nar,tr,c3) ->
if !tophyp=None then tophyp:=Some hyprecname;(* for lstatus *)
tclTHENLIST
- [ central_intro (IBasedOn (recvarname,avoid)) destopt false;
- central_intro (IBasedOn (hyprecname,avoid)) None false;
+ [ intro_gen (IBasedOn (recvarname,avoid)) destopt false;
+ intro_gen (IBasedOn (hyprecname,avoid)) None false;
peel_tac c3]
| _ -> anomaly "induct_discharge: rec arg leads to 2 products")
| IsCast (c,_) -> peel_tac c
| IsProd (na,t,c) ->
- tclTHEN (central_intro (IAvoid avoid) destopt false)
+ tclTHEN (intro_gen (IAvoid avoid) destopt false)
(peel_tac c)
| _ -> tclIDTAC
in
@@ -1076,7 +1074,7 @@ let induct_discharge indpath statuslists cname destopt avoid (_,t) =
substitutions aussi sur l'argument voisin *)
(* Marche pas... faut prendre en compte l'occurence précise... *)
-(*
+
let atomize_param_of_ind hyp0 gl =
let tmptyp0 = pf_get_hyp_typ gl hyp0 in
let (mind,indtyp,typ0) = pf_reduce_to_mind gl tmptyp0 in
@@ -1090,7 +1088,8 @@ let atomize_param_of_ind hyp0 gl =
let tmptyp0 = pf_get_hyp_typ gl hyp0 in
let (_,indtyp,_) = pf_reduce_to_mind gl tmptyp0 in
let argl = snd (decomp_app indtyp) in
- match kind_of_term (List.index argl (i-1)) with
+ let c = List.nth argl (i-1) in
+ match kind_of_term c with
| IsVar id when not (List.exists (occur_var id) avoid) ->
atomize_one (i-1) ((mkVar id)::avoid) gl
| IsVar id ->
@@ -1098,7 +1097,7 @@ let atomize_param_of_ind hyp0 gl =
tclTHEN
(letin_tac true (Name x) (mkVar id) (Some []) [])
(atomize_one (i-1) ((mkVar x)::avoid)) gl
- | c ->
+ | _ ->
let id = id_of_name_using_hdchar (Global.env()) (pf_type_of gl c)
Anonymous in
let x = fresh_id [] id gl in
@@ -1180,39 +1179,39 @@ let find_atomic_param_of_ind mind indtyp =
exception Shunt of identifier option
-let cook_sign hyp0 indvars sign =
+let cook_sign hyp0 indvars env =
(* First pass from L to R: get [indhyps], [dephyps] and [statuslist]
for the hypotheses before (= more ancient than) hyp0 (see above) *)
let allindhyps = hyp0::indvars in
let indhyps = ref [] in
- let hdeps = ref [] in
- let tdeps = ref [] in
+ let decldeps = ref [] in
let ldeps = ref [] in
let rstatus = ref [] in
let lstatus = ref [] in
let before = ref true in
- let seek_deps hyp typ rhyp =
+ let seek_deps env (hyp,_,_ as decl) rhyp =
if hyp = hyp0 then begin
before:=false;
None (* fake value *)
end else if List.mem hyp indvars then begin
indhyps := hyp::!indhyps;
rhyp
- end else if (List.exists (fun id -> occur_var id typ) allindhyps
- or List.exists (fun id -> occur_var id typ) !hdeps) then begin
- hdeps := hyp::!hdeps;
- tdeps := typ::!tdeps;
- if !before then
- rstatus := (hyp,rhyp)::!rstatus
- else
- ldeps := hyp::!ldeps; (* status calculé lors de la 2ème passe *)
- Some hyp
end else
- Some hyp
+ if (List.exists (fun id -> occur_var_in_decl id decl) allindhyps
+ or List.exists (fun (id,_,_) -> occur_var_in_decl id decl) !decldeps)
+ then begin
+ decldeps := decl::!decldeps;
+ if !before then
+ rstatus := (hyp,rhyp)::!rstatus
+ else
+ ldeps := hyp::!ldeps; (* status calculé lors de la 2ème passe *)
+ Some hyp end
+ else
+ Some hyp
in
- let _ = sign_it seek_deps sign None in
+ let _ = fold_var_context seek_deps env None in
(* 2nd pass from R to L: get left hyp of [hyp0] and [lhyps] *)
- let compute_lstatus lhyp hyp typ =
+ let compute_lstatus lhyp (hyp,_,_ as d) =
if hyp = hyp0 then raise (Shunt lhyp);
if List.mem hyp !ldeps then begin
lstatus := (hyp,lhyp)::!lstatus;
@@ -1221,11 +1220,11 @@ let cook_sign hyp0 indvars sign =
(Some hyp)
in
try
- let _ = it_sign compute_lstatus None sign in anomaly "hyp0 not found"
+ let _ = fold_var_context_reverse compute_lstatus None env in
+ anomaly "hyp0 not found"
with Shunt lhyp0 ->
let statuslists = (!lstatus,List.rev !rstatus) in
- let deps = (List.rev !hdeps, List.rev !tdeps) in
- (statuslists, lhyp0, !indhyps, deps)
+ (statuslists, lhyp0, !indhyps, !decldeps)
(* Vieille version en une seule passe grace à l'ordre supérieur mais
@@ -1282,22 +1281,22 @@ let get_constructors varname (elimc,elimt) mind mindpath =
let induction_from_context hyp0 gl =
(*test suivant sans doute inutile car protégé par le letin_tac avant appel*)
- if List.mem hyp0 (ids_of_sign (Global.var_context())) then
+ if List.mem hyp0 (ids_of_var_context (Global.var_context())) then
errorlabstrm "induction" [< 'sTR "Cannot generalize a global variable" >];
- let sign = pf_untyped_hyps gl in
- let tsign = pf_hyps gl in
- let tmptyp0 = pf_get_hyp gl hyp0 in
+ let env = pf_env gl in
+ let tmptyp0 = pf_get_hyp_typ gl hyp0 in
let ((ind_sp,_) as mind,indtyp,typ0) = pf_reduce_to_mind gl tmptyp0 in
let indvars = find_atomic_param_of_ind mind indtyp in
let mindpath = Declare.path_of_inductive_path ind_sp in
- let elimc = lookup_eliminator tsign mindpath (suff gl (pf_concl gl)) in
+ let elimc = lookup_eliminator env mindpath (sort_of_goal gl) in
let elimt = pf_type_of gl elimc in
- let (statlists,lhyp0,indhyps,deps) = cook_sign hyp0 indvars sign in
- let (dephyps,deptyps) = deps in
- let tmpcl = List.fold_right2 mkNamedProd dephyps deptyps (pf_concl gl) in
+ let (statlists,lhyp0,indhyps,deps) = cook_sign hyp0 indvars env in
+ let tmpcl = it_mkNamedProd_or_LetIn (pf_concl gl) deps in
let lc = get_constructors hyp0 (elimc,elimt) mind mindpath in
+ let dephyps = List.rev (List.map (fun (id,_,_) -> id) deps) in
+ let args = List.map mkVar dephyps in
tclTHENLIST
- [ apply_type tmpcl (List.map mkVar dephyps);
+ [ apply_type tmpcl args;
thin dephyps;
tclTHENS
(tclTHEN
@@ -1313,7 +1312,7 @@ let induction_with_atomization_of_ind_arg hyp0 =
let new_induct c gl =
match kind_of_term c with
- | IsVar id when not (List.mem id (ids_of_sign (Global.var_context()))) ->
+ | IsVar id when not (mem_var_context id (Global.var_context())) ->
tclORELSE
(tclTHEN (intros_until id) (tclLAST_HYP simplest_elim))
(induction_with_atomization_of_ind_arg id) gl
@@ -1324,7 +1323,7 @@ let new_induct c gl =
tclTHEN
(letin_tac true (Name id) c (Some []) [])
(induction_with_atomization_of_ind_arg id) gl
-*)
+
(***)
(* The registered tactic, which calls the default elimination
@@ -1345,28 +1344,23 @@ let dyn_elim = function
| l -> bad_tactic_args "elim" l
(* Induction tactics *)
-(*
let induct s =
tclORELSE (tclTHEN (intros_until s) (tclLAST_HYP simplest_elim))
(induction_from_context s)
-*)
-let induct s =
- tclTHEN (intros_until s) (tclLAST_HYP simplest_elim)
-
let induct_nodep n = tclTHEN (intros_do n) (tclLAST_HYP simplest_elim)
(* Pour le futur
let dyn_induct = function
- | [(COMMAND c)] -> tactic_com new_induct x
- | [(CONSTR x)] -> new_induct x
- | [(INTEGER n)] -> induct_nodep n
+ | [(Command c)] -> tactic_com new_induct x
+ | [(Constr x)] -> new_induct x
+ | [(Integer n)] -> induct_nodep n
| l -> bad_tactic_args "induct" l
*)
let dyn_induct = function
- | [Identifier x] -> induct x
- | [Integer n] -> induct_nodep n
+ | [Identifier x] -> induct x
+ | [Integer n] -> induct_nodep n
| l -> bad_tactic_args "induct" l
(* Case analysis tactics *)
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 06:51:34 +0000