diff options
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/hiddentac.ml | 6 | ||||
| -rw-r--r-- | tactics/hiddentac.mli | 4 | ||||
| -rw-r--r-- | tactics/inv.ml | 2 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 21 | ||||
| -rw-r--r-- | tactics/tactics.ml | 17 | ||||
| -rw-r--r-- | tactics/tactics.mli | 2 |
6 files changed, 28 insertions, 24 deletions
diff --git a/tactics/hiddentac.ml b/tactics/hiddentac.ml index ebcddc71c..5b35fcb86 100644 --- a/tactics/hiddentac.ml +++ b/tactics/hiddentac.ml @@ -40,12 +40,12 @@ let h_mutual_cofix id l = abstract_tactic (TacMutualCofix (id,l)) (mutual_cofix id l) let h_cut c = abstract_tactic (TacCut c) (cut c) -let h_true_cut ido c = abstract_tactic (TacTrueCut (ido,c)) (true_cut ido c) +let h_true_cut na c = abstract_tactic (TacTrueCut (na,c)) (true_cut na c) let h_forward b na c = abstract_tactic (TacForward (b,na,c)) (forward b na c) let h_generalize cl = abstract_tactic (TacGeneralize cl) (generalize cl) let h_generalize_dep c = abstract_tactic (TacGeneralizeDep c)(generalize_dep c) -let h_let_tac id c cl = - abstract_tactic (TacLetTac (id,c,cl)) (letin_tac true (Names.Name id) c cl) +let h_let_tac na c cl = + abstract_tactic (TacLetTac (na,c,cl)) (letin_tac true na c cl) let h_instantiate n c cls = abstract_tactic (TacInstantiate (n,c,cls)) (Evar_refiner.instantiate n c (simple_clause_of cls)) diff --git a/tactics/hiddentac.mli b/tactics/hiddentac.mli index 1ea438874..364e21969 100644 --- a/tactics/hiddentac.mli +++ b/tactics/hiddentac.mli @@ -44,11 +44,11 @@ val h_mutual_cofix : identifier -> (identifier * constr) list -> tactic val h_cofix : identifier option -> tactic val h_cut : constr -> tactic -val h_true_cut : identifier option -> constr -> tactic +val h_true_cut : name -> constr -> tactic val h_generalize : constr list -> tactic val h_generalize_dep : constr -> tactic val h_forward : bool -> name -> constr -> tactic -val h_let_tac : identifier -> constr -> Tacticals.clause -> tactic +val h_let_tac : name -> constr -> Tacticals.clause -> tactic val h_instantiate : int -> constr -> Tacticals.clause -> tactic (* Derived basic tactics *) diff --git a/tactics/inv.ml b/tactics/inv.ml index fddcf4761..2902f37e0 100644 --- a/tactics/inv.ml +++ b/tactics/inv.ml @@ -467,7 +467,7 @@ let raw_inversion inv_kind indbinding id status names gl = case_nodep_then_using in (tclTHENS - (true_cut None cut_concl) + (true_cut Anonymous cut_concl) [case_tac names (introCaseAssumsThen (rewrite_equations_tac inv_kind id neqns)) (Some elim_predicate) ([],[]) newc; diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index eff274988..2217dbe10 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -608,14 +608,15 @@ let rec intern_atomic lf ist x = let f (id,c) = (intern_ident lf ist id,intern_constr ist c) in TacMutualCofix (intern_ident lf ist id, List.map f l) | TacCut c -> TacCut (intern_constr ist c) - | TacTrueCut (ido,c) -> - TacTrueCut (option_app (intern_ident lf ist) ido, intern_constr ist c) - | TacForward (b,na,c) -> TacForward (b,intern_name lf ist na,intern_constr ist c) + | TacTrueCut (na,c) -> + TacTrueCut (intern_name lf ist na, intern_constr ist c) + | TacForward (b,na,c) -> + TacForward (b,intern_name lf ist na,intern_constr ist c) | TacGeneralize cl -> TacGeneralize (List.map (intern_constr ist) cl) | TacGeneralizeDep c -> TacGeneralizeDep (intern_constr ist c) - | TacLetTac (id,c,cls) -> - let id = intern_ident lf ist id in - TacLetTac (id,intern_constr ist c, + | TacLetTac (na,c,cls) -> + let na = intern_name lf ist na in + TacLetTac (na,intern_constr ist c, (clause_app (intern_hyp_location ist) cls)) | TacInstantiate (n,c,cls) -> TacInstantiate (n,intern_constr ist c, @@ -1621,15 +1622,15 @@ and interp_atomic ist gl = function let f (id,c) = (eval_ident ist id,pf_interp_constr ist gl c) in h_mutual_cofix (eval_ident ist id) (List.map f l) | TacCut c -> h_cut (pf_interp_constr ist gl c) - | TacTrueCut (ido,c) -> - h_true_cut (eval_opt_ident ist ido) (pf_interp_constr ist gl c) + | TacTrueCut (na,c) -> + h_true_cut (eval_name ist na) (pf_interp_constr ist gl c) | TacForward (b,na,c) -> h_forward b (eval_name ist na) (pf_interp_constr ist gl c) | TacGeneralize cl -> h_generalize (List.map (pf_interp_constr ist gl) cl) | TacGeneralizeDep c -> h_generalize_dep (pf_interp_constr ist gl c) - | TacLetTac (id,c,clp) -> + | TacLetTac (na,c,clp) -> let clp = interp_clause ist gl clp in - h_let_tac (eval_ident ist id) (pf_interp_constr ist gl c) clp + h_let_tac (eval_name ist na) (pf_interp_constr ist gl c) clp | TacInstantiate (n,c,ido) -> h_instantiate n (pf_interp_constr ist gl c) (clause_app (interp_hyp_location ist gl) ido) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 2084cac2a..d739cb225 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -505,15 +505,15 @@ let cut_and_apply c gl = (* Cut tactics *) (**************************) -let true_cut idopt c gl = +let true_cut na c gl = match kind_of_term (hnf_type_of gl c) with | Sort s -> let id = - match idopt with - | None -> + match na with + | Anonymous -> let d = match s with Prop _ -> "H" | Type _ -> "X" in fresh_id [] (id_of_string d) gl - | Some id -> id + | Name id -> id in internal_cut id c gl | _ -> error "Not a proposition or a type" @@ -759,9 +759,12 @@ let check_hypotheses_occurrences_list env (_,occl) = let nowhere = {onhyps=Some[]; onconcl=false; concl_occs=[]} -(* Tactic Pose should not perform any replacement (as specified in - the doc), but it does in the conclusion! *) -let forward b na c = letin_tac b na c onConcl +(* Tactic Assert (b=false) and Pose (b=true): + the behaviour of Pose is corrected by the translator. + not that of Assert *) +let forward b na c = + let wh = if !Options.v7 && b then onConcl else nowhere in + letin_tac b na c wh (********************************************************************) (* Exact tactics *) diff --git a/tactics/tactics.mli b/tactics/tactics.mli index f5c761994..ee65f1332 100644 --- a/tactics/tactics.mli +++ b/tactics/tactics.mli @@ -234,7 +234,7 @@ val cut_intro : constr -> tactic val cut_replacing : identifier -> constr -> tactic val cut_in_parallel : constr list -> tactic -val true_cut : identifier option -> constr -> tactic +val true_cut : name -> constr -> tactic val letin_tac : bool -> name -> constr -> clause -> tactic val forward : bool -> name -> constr -> tactic val generalize : constr list -> tactic |