diff options
author | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:08:41 +0000 |
---|---|---|
committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-05-29 11:08:41 +0000 |
commit | b31b48407a9f5d36cefd6dec3ddf3e0b8391f14c (patch) | |
tree | 27348cbd7525d2affcd4b871db09a510de52c616 | |
parent | 5fa47f1258408541150e2e4c26d60ff694e7c1bc (diff) |
Tacexpr as a mli-only, the few functions there are now in Tacops
NB: former Tacexpr.no_move is now Tacexpr.MoveLast
(when introducing, intro with no move is intro as last)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15373 85f007b7-540e-0410-9357-904b9bb8a0f7
-rw-r--r-- | dev/printers.mllib | 2 | ||||
-rw-r--r-- | intf/tacexpr.mli (renamed from proofs/tacexpr.ml) | 34 | ||||
-rw-r--r-- | parsing/g_tactic.ml4 | 12 | ||||
-rw-r--r-- | parsing/grammar.mllib | 2 | ||||
-rw-r--r-- | parsing/pptactic.ml | 10 | ||||
-rw-r--r-- | parsing/printer.ml | 2 | ||||
-rw-r--r-- | parsing/q_coqast.ml4 | 3 | ||||
-rw-r--r-- | plugins/xml/proofTree2Xml.ml4 | 3 | ||||
-rw-r--r-- | proofs/logic.ml | 8 | ||||
-rw-r--r-- | proofs/proofs.mllib | 2 | ||||
-rw-r--r-- | proofs/tacops.ml | 51 | ||||
-rw-r--r-- | proofs/tacops.mli | 14 | ||||
-rw-r--r-- | tactics/elim.ml | 2 | ||||
-rw-r--r-- | tactics/equality.ml | 2 | ||||
-rw-r--r-- | tactics/hiddentac.ml | 2 | ||||
-rw-r--r-- | tactics/inv.ml | 12 | ||||
-rw-r--r-- | tactics/tacinterp.ml | 8 | ||||
-rw-r--r-- | tactics/tactics.ml | 54 |
18 files changed, 130 insertions, 93 deletions
diff --git a/dev/printers.mllib b/dev/printers.mllib index 8ba207000..436fa287f 100644 --- a/dev/printers.mllib +++ b/dev/printers.mllib @@ -115,7 +115,7 @@ Smartlocate Constrintern Modintern Constrextern -Tacexpr +Tacops Proof_type Goal Logic diff --git a/proofs/tacexpr.ml b/intf/tacexpr.mli index 4f960243c..16ba9f95e 100644 --- a/proofs/tacexpr.ml +++ b/intf/tacexpr.mli @@ -40,43 +40,13 @@ type glob_red_flag = | FConst of reference or_by_notation list | FDeltaBut of reference or_by_notation list -let make_red_flag = - let rec add_flag red = function - | [] -> red - | FBeta :: lf -> add_flag { red with rBeta = true } lf - | FIota :: lf -> add_flag { red with rIota = true } lf - | FZeta :: lf -> add_flag { red with rZeta = true } lf - | FConst l :: lf -> - if red.rDelta then - error - "Cannot set both constants to unfold and constants not to unfold"; - add_flag { red with rConst = list_union red.rConst l } lf - | FDeltaBut l :: lf -> - if red.rConst <> [] & not red.rDelta then - error - "Cannot set both constants to unfold and constants not to unfold"; - add_flag - { red with rConst = list_union red.rConst l; rDelta = true } - lf - in - add_flag - {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} - type 'a raw_hyp_location = 'a with_occurrences * hyp_location_flag type 'id move_location = | MoveAfter of 'id | MoveBefore of 'id - | MoveToEnd of bool - -let no_move = MoveToEnd true - -open Pp - -let pr_move_location pr_id = function - | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id - | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id - | MoveToEnd toleft -> str (if toleft then " at bottom" else " at top") + | MoveFirst + | MoveLast (* can be seen as "no move" when doing intro *) type 'a induction_arg = | ElimOnConstr of 'a diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 7cbcd584c..55c03a481 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -22,7 +22,7 @@ open Misctypes open Locus open Decl_kinds -let all_with delta = make_red_flag [FBeta;FIota;FZeta;delta] +let all_with delta = Tacops.make_red_flag [FBeta;FIota;FZeta;delta] let tactic_kw = [ "->"; "<-" ; "by" ] let _ = List.iter Lexer.add_keyword tactic_kw @@ -327,7 +327,7 @@ GEXTEND Gram ] ] ; strategy_flag: - [ [ s = LIST1 red_flag -> make_red_flag s + [ [ s = LIST1 red_flag -> Tacops.make_red_flag s | d = delta_flag -> all_with d ] ] ; @@ -503,8 +503,8 @@ GEXTEND Gram move_location: [ [ IDENT "after"; id = id_or_meta -> MoveAfter id | IDENT "before"; id = id_or_meta -> MoveBefore id - | "at"; IDENT "bottom" -> MoveToEnd true - | "at"; IDENT "top" -> MoveToEnd false ] ] + | "at"; IDENT "top" -> MoveFirst + | "at"; IDENT "bottom" -> MoveLast ] ] ; simple_tactic: [ [ @@ -515,8 +515,8 @@ GEXTEND Gram | IDENT "intro"; id = ident; hto = move_location -> TacIntroMove (Some id, hto) | IDENT "intro"; hto = move_location -> TacIntroMove (None, hto) - | IDENT "intro"; id = ident -> TacIntroMove (Some id, no_move) - | IDENT "intro" -> TacIntroMove (None, no_move) + | IDENT "intro"; id = ident -> TacIntroMove (Some id, MoveLast) + | IDENT "intro" -> TacIntroMove (None, MoveLast) | IDENT "assumption" -> TacAssumption | IDENT "exact"; c = constr -> TacExact c diff --git a/parsing/grammar.mllib b/parsing/grammar.mllib index cae4b13d6..caf3d8508 100644 --- a/parsing/grammar.mllib +++ b/parsing/grammar.mllib @@ -69,7 +69,7 @@ Pattern Topconstr Genarg Ppextend -Tacexpr +Tacops Tok Lexer Extend diff --git a/parsing/pptactic.ml b/parsing/pptactic.ml index c50ab9fcd..58ce29a04 100644 --- a/parsing/pptactic.ml +++ b/parsing/pptactic.ml @@ -624,7 +624,7 @@ let pr_cofix_tac (id,c) = (* Printing tactics as arguments *) let rec pr_atom0 = function | TacIntroPattern [] -> str "intros" - | TacIntroMove (None,hto) when hto = no_move -> str "intro" + | TacIntroMove (None,MoveLast) -> str "intro" | TacAssumption -> str "assumption" | TacAnyConstructor (false,None) -> str "constructor" | TacAnyConstructor (true,None) -> str "econstructor" @@ -647,10 +647,10 @@ and pr_atom1 = function hov 1 (str "intros" ++ spc () ++ prlist_with_sep spc pr_intro_pattern p) | TacIntrosUntil h -> hv 1 (str "intros until" ++ pr_arg pr_quantified_hypothesis h) - | TacIntroMove (None,hto) as t when hto = no_move -> pr_atom0 t - | TacIntroMove (Some id,hto) when hto = no_move -> str "intro " ++ pr_id id + | TacIntroMove (None,MoveLast) as t -> pr_atom0 t + | TacIntroMove (Some id,MoveLast) -> str "intro " ++ pr_id id | TacIntroMove (ido,hto) -> - hov 1 (str"intro" ++ pr_opt pr_id ido ++ pr_move_location pr_ident hto) + hov 1 (str"intro" ++ pr_opt pr_id ido ++ Tacops.pr_move_location pr_ident hto) | TacAssumption as t -> pr_atom0 t | TacExact c -> hov 1 (str "exact" ++ pr_constrarg c) | TacExactNoCheck c -> hov 1 (str "exact_no_check" ++ pr_constrarg c) @@ -764,7 +764,7 @@ and pr_atom1 = function assert b; hov 1 (str "move" ++ brk (1,1) ++ pr_ident id1 ++ - pr_move_location pr_ident id2) + Tacops.pr_move_location pr_ident id2) | TacRename l -> hov 1 (str "rename" ++ brk (1,1) ++ diff --git a/parsing/printer.ml b/parsing/printer.ml index b63e804d2..20fbda2d7 100644 --- a/parsing/printer.ml +++ b/parsing/printer.ml @@ -519,7 +519,7 @@ let pr_prim_rule = function | Move (withdep,id1,id2) -> (str (if withdep then "dependent " else "") ++ - str"move " ++ pr_id id1 ++ pr_move_location pr_id id2) + str"move " ++ pr_id id1 ++ Tacops.pr_move_location pr_id id2) | Order ord -> (str"order " ++ pr_sequence pr_id ord) diff --git a/parsing/q_coqast.ml4 b/parsing/q_coqast.ml4 index 6ef7ba1d8..c4581fe1e 100644 --- a/parsing/q_coqast.ml4 +++ b/parsing/q_coqast.ml4 @@ -238,7 +238,8 @@ let mlexpr_of_constr_with_binding = let mlexpr_of_move_location f = function | Tacexpr.MoveAfter id -> <:expr< Tacexpr.MoveAfter $f id$ >> | Tacexpr.MoveBefore id -> <:expr< Tacexpr.MoveBefore $f id$ >> - | Tacexpr.MoveToEnd b -> <:expr< Tacexpr.MoveToEnd $mlexpr_of_bool b$ >> + | Tacexpr.MoveFirst -> <:expr< Tacexpr.MoveFirst >> + | Tacexpr.MoveLast -> <:expr< Tacexpr.MoveLast >> let mlexpr_of_induction_arg = function | Tacexpr.ElimOnConstr c -> diff --git a/plugins/xml/proofTree2Xml.ml4 b/plugins/xml/proofTree2Xml.ml4 index 21058a7b9..a45b8cda4 100644 --- a/plugins/xml/proofTree2Xml.ml4 +++ b/plugins/xml/proofTree2Xml.ml4 @@ -96,7 +96,6 @@ let let module PT = Proof_type in let module L = Logic in let module X = Xml in - let module T = Tacexpr in let ids_of_node node = let constr = Proof2aproof.ProofTreeHash.find proof_tree_to_constr node in (* @@ -144,7 +143,7 @@ Pp.ppnl (Pp.(++) (Pp.str Proof2aproof.ProofTreeHash.find proof_tree_to_flattened_proof_tree node in begin match tactic_expr with - | T.TacArg (_,T.Tacexp _) -> + | Tacexpr.TacArg (_,Tacexpr.Tacexp _) -> (* We don't need to keep the level of abstraction introduced at *) (* user-level invocation of tactic... (see Tacinterp.hide_interp)*) aux flat_proof old_hyps diff --git a/proofs/logic.ml b/proofs/logic.ml index c7df86e1f..3361752ed 100644 --- a/proofs/logic.ml +++ b/proofs/logic.ml @@ -221,7 +221,7 @@ let rec get_hyp_after h = function | [] -> error_no_such_hypothesis h | (hyp,_,_) :: right -> if hyp = h then - match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveToEnd false + match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveFirst else get_hyp_after h right @@ -230,7 +230,7 @@ let split_sign hfrom hto l = | [] -> error_no_such_hypothesis hfrom | (hyp,c,typ) as d :: right -> if hyp = hfrom then - (left,right,d, toleft or hto = MoveToEnd true) + (left,right,d, toleft or hto = MoveLast) else splitrec (d::left) (toleft or hto = MoveAfter hyp or hto = MoveBefore hyp) @@ -252,7 +252,7 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = in let rec moverec first middle = function | [] -> - if match hto with MoveToEnd _ -> false | _ -> true then + if match hto with MoveFirst | MoveLast -> false | _ -> true then error_no_such_hypothesis (hyp_of_move_location hto); List.rev first @ List.rev middle | (hyp,_,_) :: _ as right when hto = MoveBefore hyp -> @@ -264,7 +264,7 @@ let move_hyp with_dep toleft (left,(idfrom,_,_ as declfrom),right) hto = (first, d::middle) else errorlabstrm "move_hyp" (str "Cannot move " ++ pr_id idfrom ++ - pr_move_location pr_id hto ++ + Tacops.pr_move_location pr_id hto ++ str (if toleft then ": it occurs in " else ": it depends on ") ++ pr_id hyp ++ str ".") else diff --git a/proofs/proofs.mllib b/proofs/proofs.mllib index 66001e77a..6b8fbf24b 100644 --- a/proofs/proofs.mllib +++ b/proofs/proofs.mllib @@ -3,7 +3,7 @@ Evar_refiner Proofview Proof Proof_global -Tacexpr +Tacops Proof_type Redexpr Logic diff --git a/proofs/tacops.ml b/proofs/tacops.ml new file mode 100644 index 000000000..05c4e6093 --- /dev/null +++ b/proofs/tacops.ml @@ -0,0 +1,51 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +open Names +open Topconstr +open Libnames +open Nametab +open Glob_term +open Errors +open Util +open Genarg +open Pattern +open Decl_kinds +open Misctypes +open Locus +open Tacexpr + +let make_red_flag = + let rec add_flag red = function + | [] -> red + | FBeta :: lf -> add_flag { red with rBeta = true } lf + | FIota :: lf -> add_flag { red with rIota = true } lf + | FZeta :: lf -> add_flag { red with rZeta = true } lf + | FConst l :: lf -> + if red.rDelta then + error + "Cannot set both constants to unfold and constants not to unfold"; + add_flag { red with rConst = list_union red.rConst l } lf + | FDeltaBut l :: lf -> + if red.rConst <> [] & not red.rDelta then + error + "Cannot set both constants to unfold and constants not to unfold"; + add_flag + { red with rConst = list_union red.rConst l; rDelta = true } + lf + in + add_flag + {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} + +open Pp + +let pr_move_location pr_id = function + | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id + | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id + | MoveFirst -> str " at top" + | MoveLast -> str " at bottom" diff --git a/proofs/tacops.mli b/proofs/tacops.mli new file mode 100644 index 000000000..be17e035a --- /dev/null +++ b/proofs/tacops.mli @@ -0,0 +1,14 @@ +(************************************************************************) +(* v * The Coq Proof Assistant / The Coq Development Team *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2010 *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(************************************************************************) + +val make_red_flag : + Tacexpr.glob_red_flag list -> + (Libnames.reference Misctypes.or_by_notation) Glob_term.glob_red_flag + +val pr_move_location : + ('a -> Pp.std_ppcmds) -> 'a Tacexpr.move_location -> Pp.std_ppcmds diff --git a/tactics/elim.ml b/tactics/elim.ml index aa13d27b1..bd304d975 100644 --- a/tactics/elim.ml +++ b/tactics/elim.ml @@ -49,7 +49,7 @@ let introCaseAssumsThen tac ba = (ba.branchnames, []), if n1 > n2 then snd (list_chop n2 case_thin_sign) else [] in let introCaseAssums = - tclTHEN (intros_pattern no_move l1) (intros_clearing l3) in + tclTHEN (intros_pattern MoveLast l1) (intros_clearing l3) in (tclTHEN introCaseAssums (case_on_ba (tac l2) ba)) (* The following tactic Decompose repeatedly applies the diff --git a/tactics/equality.ml b/tactics/equality.ml index 03f3811b7..cfbb30a74 100644 --- a/tactics/equality.ml +++ b/tactics/equality.ml @@ -1160,7 +1160,7 @@ let injEq ipats (eq,_,(t,t1,t2) as u) eq_clause = ) else (raise Not_dep_pair) ) with _ -> inject_at_positions env sigma u eq_clause posns - (fun _ -> intros_pattern no_move ipats) + (fun _ -> intros_pattern MoveLast ipats) let inj ipats with_evars = onEquality with_evars (injEq ipats) diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index 8410e08cc..d1d3d90c5 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -22,7 +22,7 @@ open Misctypes (* Basic tactics *) let h_intro_move x y = abstract_tactic (TacIntroMove (x, y)) (intro_move x y) -let h_intro x = h_intro_move (Some x) no_move +let h_intro x = h_intro_move (Some x) MoveLast let h_intros_until x = abstract_tactic (TacIntrosUntil x) (intros_until x) let h_assumption = abstract_tactic TacAssumption assumption let h_exact c = abstract_tactic (TacExact c) (exact_check c) diff --git a/tactics/inv.ml b/tactics/inv.ml index f5762768e..f1f844076 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -295,7 +295,7 @@ let rec tclMAP_i n tacfun = function if n=0 then error "Too many names." else tclTHEN (tacfun (Some a)) (tclMAP_i (n-1) tacfun l) -let remember_first_eq id x = if !x = no_move then x := MoveAfter id +let remember_first_eq id x = if !x = MoveLast then x := MoveAfter id (* invariant: ProjectAndApply is responsible for erasing the clause which it is given as input @@ -322,7 +322,7 @@ let projectAndApply thin id eqname names depids gls = [(if names <> [] then clear [id] else tclIDTAC); (tclMAP_i neqns (fun idopt -> tclTRY (tclTHEN - (intro_move idopt no_move) + (intro_move idopt MoveLast) (* try again to substitute and if still not a variable after *) (* decomposition, arbitrarily try to rewrite RL !? *) (tclTRY (onLastHypId (substHypIfVariable (subst_hyp false)))))) @@ -353,7 +353,7 @@ let rewrite_equations_gene othin neqns ba gl = (onLastHypId (fun id -> tclTRY - (projectAndApply thin id (ref no_move) + (projectAndApply thin id (ref MoveLast) [] depids)))); onHyps (compose List.rev (afterHyp last)) bring_hyps; onHyps (afterHyp last) @@ -407,7 +407,7 @@ let rewrite_equations othin neqns names ba gl = let names = List.map (get_names true) names in let (depids,nodepids) = split_dep_and_nodep ba.assums gl in let rewrite_eqns = - let first_eq = ref no_move in + let first_eq = ref MoveLast in match othin with | Some thin -> tclTHENSEQ @@ -416,12 +416,12 @@ let rewrite_equations othin neqns names ba gl = tclMAP_i neqns (fun o -> let idopt,names = extract_eqn_names o in (tclTHEN - (intro_move idopt no_move) + (intro_move idopt MoveLast) (onLastHypId (fun id -> tclTRY (projectAndApply thin id first_eq names depids))))) names; tclMAP (fun (id,_,_) gl -> - intro_move None (if thin then no_move else !first_eq) gl) + intro_move None (if thin then MoveLast else !first_eq) gl) nodepids; tclMAP (fun (id,_,_) -> tclTRY (clear [id])) depids] | None -> tclIDTAC diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index 0d277855f..f3b6c58c0 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -173,7 +173,7 @@ let _ = "hnf", TacReduce(Hnf,nocl); "simpl", TacReduce(Simpl None,nocl); "compute", TacReduce(Cbv all_flags,nocl); - "intro", TacIntroMove(None,no_move); + "intro", TacIntroMove(None,MoveLast); "intros", TacIntroPattern []; "assumption", TacAssumption; "cofix", TacCofix None; @@ -384,7 +384,8 @@ let intern_constr_reference strict ist = function let intern_move_location ist = function | MoveAfter id -> MoveAfter (intern_hyp_or_metaid ist id) | MoveBefore id -> MoveBefore (intern_hyp_or_metaid ist id) - | MoveToEnd toleft as x -> x + | MoveFirst -> MoveFirst + | MoveLast -> MoveLast (* Internalize an isolated reference in position of tactic *) @@ -1130,7 +1131,8 @@ let interp_hyp_list ist gl l = let interp_move_location ist gl = function | MoveAfter id -> MoveAfter (interp_hyp ist gl id) | MoveBefore id -> MoveBefore (interp_hyp ist gl id) - | MoveToEnd toleft as x -> x + | MoveFirst -> MoveFirst + | MoveLast -> MoveLast (* Interprets a qualified name *) let coerce_to_reference env v = diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 7e350bfe9..897e1d7ef 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -425,7 +425,7 @@ let find_intro_names ctxt gl = List.rev res let build_intro_tac id dest tac = match dest with - | MoveToEnd true -> tclTHEN (introduction id) (tac id) + | MoveLast -> tclTHEN (introduction id) (tac id) | dest -> tclTHENLIST [introduction id; move_hyp true id dest; tac id] let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac gl = @@ -444,14 +444,14 @@ let rec intro_then_gen loc name_flag move_flag force_flag dep_flag tac gl = user_err_loc(loc,"Intro",str "No product even after head-reduction.") let intro_gen loc n m f d = intro_then_gen loc n m f d (fun _ -> tclIDTAC) -let intro_mustbe_force id = intro_gen dloc (IntroMustBe id) no_move true false -let intro_using id = intro_gen dloc (IntroBasedOn (id,[])) no_move false false -let intro_then = intro_then_gen dloc (IntroAvoid []) no_move false false -let intro = intro_gen dloc (IntroAvoid []) no_move false false -let introf = intro_gen dloc (IntroAvoid []) no_move true false -let intro_avoiding l = intro_gen dloc (IntroAvoid l) no_move false false +let intro_mustbe_force id = intro_gen dloc (IntroMustBe id) MoveLast true false +let intro_using id = intro_gen dloc (IntroBasedOn (id,[])) MoveLast false false +let intro_then = intro_then_gen dloc (IntroAvoid []) MoveLast false false +let intro = intro_gen dloc (IntroAvoid []) MoveLast false false +let introf = intro_gen dloc (IntroAvoid []) MoveLast true false +let intro_avoiding l = intro_gen dloc (IntroAvoid l) MoveLast false false -let intro_then_force = intro_then_gen dloc (IntroAvoid []) no_move true false +let intro_then_force = intro_then_gen dloc (IntroAvoid []) MoveLast true false (**** Multiple introduction tactics ****) @@ -475,7 +475,7 @@ let rec get_next_hyp_position id = function | [] -> error ("No such hypothesis: " ^ string_of_id id) | (hyp,_,_) :: right -> if hyp = id then - match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveToEnd true + match right with (id,_,_)::_ -> MoveBefore id | [] -> MoveLast else get_next_hyp_position id right @@ -1362,7 +1362,7 @@ let check_thin_clash_then id thin avoid tac = let rec intros_patterns b avoid ids thin destopt tac = function | (loc, IntroWildcard) :: l -> intro_then_gen loc (IntroBasedOn(wild_id,avoid@explicit_intro_names l)) - no_move true false + MoveLast true false (fun id -> intros_patterns b avoid ids ((loc,id)::thin) destopt tac l) | (loc, IntroIdentifier id) :: l -> check_thin_clash_then id thin avoid (fun thin -> @@ -1387,7 +1387,7 @@ let rec intros_patterns b avoid ids thin destopt tac = function (intros_patterns b avoid ids thin destopt tac)) | (loc, IntroRewrite l2r) :: l -> intro_then_gen loc (IntroAvoid(avoid@explicit_intro_names l)) - no_move true false + MoveLast true false (fun id -> tclTHENLAST (* Skip the side conditions of the rewriting step *) (rewrite_hyp l2r id) @@ -1402,7 +1402,7 @@ let intro_pattern destopt pat = let intro_patterns = function | [] -> tclREPEAT intro - | l -> intros_pattern no_move l + | l -> intros_pattern MoveLast l (**************************) (* Other cut tactics *) @@ -1423,7 +1423,7 @@ let prepare_intros s ipat gl = match ipat with | IntroOrAndPattern ll -> make_id s gl, onLastHypId (intro_or_and_pattern loc true ll [] - (intros_patterns true [] [] [] no_move (fun _ -> clear_wildcards))) + (intros_patterns true [] [] [] MoveLast (fun _ -> clear_wildcards))) | IntroForthcoming _ -> user_err_loc (loc,"",str "Introduction pattern for one hypothesis expected") @@ -1457,7 +1457,7 @@ let as_tac id ipat = match ipat with !forward_general_multi_rewrite l2r false (mkVar id,NoBindings) allHypsAndConcl | Some (loc,IntroOrAndPattern ll) -> intro_or_and_pattern loc true ll [] - (intros_patterns true [] [] [] no_move (fun _ -> clear_wildcards)) + (intros_patterns true [] [] [] MoveLast (fun _ -> clear_wildcards)) id | Some (loc, (IntroIdentifier _ | IntroAnonymous | IntroFresh _ | @@ -1748,7 +1748,7 @@ let letin_abstract id c (test,out) (occs,check_occs) gl = | Some occ -> subst1 (mkVar id) (subst_closed_term_occ_modulo occ test None (pf_concl gl)) in let lastlhyp = - if depdecls = [] then no_move else MoveAfter(pi1(list_last depdecls)) in + if depdecls = [] then MoveLast else MoveAfter(pi1(list_last depdecls)) in (depdecls,lastlhyp,ccl,out test) let letin_tac_gen with_eq name (sigmac,c) test ty occs gl = @@ -1895,15 +1895,15 @@ let rec consume_pattern avoid id isdep gl = function | pat::names -> (pat,names) let re_intro_dependent_hypotheses (lstatus,rstatus) (_,tophyp) = - let tophyp = match tophyp with None -> MoveToEnd true | Some hyp -> MoveAfter hyp in + let tophyp = match tophyp with None -> MoveLast | Some hyp -> MoveAfter hyp in let newlstatus = (* if some IH has taken place at the top of hyps *) - List.map (function (hyp,MoveToEnd true) -> (hyp,tophyp) | x -> x) lstatus + List.map (function (hyp,MoveLast) -> (hyp,tophyp) | x -> x) lstatus in tclTHEN (intros_move rstatus) (intros_move newlstatus) -let update destopt tophyp = if destopt = no_move then tophyp else destopt +let update destopt tophyp = if destopt = MoveLast then tophyp else destopt let safe_dest_intros_patterns avoid thin dest pat tac gl = try intros_patterns true avoid [] thin dest tac pat gl @@ -1912,7 +1912,7 @@ let safe_dest_intros_patterns avoid thin dest pat tac gl = only after cook_sign is called, e.g. as in "destruct dec" in context "dec:forall x, {x=0}+{x<>0}; a:A |- if dec a then True else False" where argument a of dec will be found only lately *) - intros_patterns true avoid [] [] no_move tac pat gl + intros_patterns true avoid [] [] MoveLast tac pat gl type elim_arg_kind = RecArg | IndArg | OtherArg @@ -1929,7 +1929,7 @@ let update_dest (recargdests,tophyp as dests) = function let get_recarg_dest (recargdests,tophyp) = match recargdests with - | AfterFixedPosition None -> MoveToEnd true + | AfterFixedPosition None -> MoveLast | AfterFixedPosition (Some id) -> MoveAfter id (* Current policy re-introduces recursive arguments of destructed @@ -1956,13 +1956,13 @@ let induct_discharge dests avoid' tac (avoid,ra) names gl = let hyprec,names = consume_pattern avoid hyprecname depind gl names in let dest = get_recarg_dest dests in safe_dest_intros_patterns avoid thin dest [recpat] (fun ids thin -> - safe_dest_intros_patterns avoid thin no_move [hyprec] (fun ids' thin -> + safe_dest_intros_patterns avoid thin MoveLast [hyprec] (fun ids' thin -> peel_tac ra' (update_dest dests ids') names thin)) gl | (IndArg,dep,hyprecname) :: ra' -> (* Rem: does not happen in Coq schemes, only in user-defined schemes *) let pat,names = consume_pattern avoid hyprecname dep gl names in - safe_dest_intros_patterns avoid thin no_move [pat] (fun ids thin -> + safe_dest_intros_patterns avoid thin MoveLast [pat] (fun ids thin -> peel_tac ra' (update_dest dests ids) names thin) gl | (RecArg,dep,recvarname) :: ra' -> let pat,names = consume_pattern avoid recvarname dep gl names in @@ -2123,7 +2123,7 @@ let cook_sign hyp0_opt indvars env = (* If there was no main induction hypotheses, then hyp is one of indvars too, so add it to indhyps. *) (if hyp0_opt=None then indhyps := hyp::!indhyps); - MoveToEnd false (* fake value *) + MoveFirst (* fake value *) end else if List.mem hyp indvars then begin (* warning: hyp can still occur after induction *) (* e.g. if the goal (t hyp hyp0) with other occs of hyp in t *) @@ -2143,7 +2143,7 @@ let cook_sign hyp0_opt indvars env = else MoveBefore hyp in - let _ = fold_named_context seek_deps env ~init:(MoveToEnd false) in + let _ = fold_named_context seek_deps env ~init:MoveFirst in (* 2nd phase from R to L: get left hyp of [hyp0] and [lhyps] *) let compute_lstatus lhyp (hyp,_,_) = if hyp = hyp0 then raise (Shunt lhyp); @@ -2155,11 +2155,11 @@ let cook_sign hyp0_opt indvars env = in try let _ = - fold_named_context_reverse compute_lstatus ~init:(MoveToEnd true) env in - raise (Shunt (MoveToEnd true)) (* ?? FIXME *) + fold_named_context_reverse compute_lstatus ~init:MoveLast env in + raise (Shunt MoveLast) (* ?? FIXME *) with Shunt lhyp0 -> let lhyp0 = match lhyp0 with - | MoveToEnd true -> None + | MoveLast -> None | MoveAfter hyp -> Some hyp | _ -> assert false in let statuslists = (!lstatus,List.rev !rstatus) in |