diff options
| author | Pierre-Marie Pédrot | 2014-05-20 19:56:29 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-05-20 20:03:00 +0200 |
| commit | bf18afeefa06e972c6cb98fa8a81ec7172fdde7f (patch) | |
| tree | 78b737079c541e425c160506d9b80577f389f091 /tactics | |
| parent | b6fea49600a5b6089eeeea877f06f0e197a0eafb (diff) | |
Moving (e)transitivity out of the AST.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/coretactics.ml4 | 8 | ||||
| -rw-r--r-- | tactics/tacintern.ml | 1 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 6 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 1 |
4 files changed, 8 insertions, 8 deletions
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4 index d3b9dd1325..f033ef5caf 100644 --- a/tactics/coretactics.ml4 +++ b/tactics/coretactics.ml4 @@ -23,6 +23,10 @@ TACTIC EXTEND assumption [ "assumption" ] -> [ Tactics.assumption ] END +TACTIC EXTEND etransitivity + [ "etransitivity" ] -> [ Tactics.intros_transitivity None ] +END + TACTIC EXTEND cut [ "cut" constr(c) ] -> [ Tactics.cut c ] END @@ -46,3 +50,7 @@ END TACTIC EXTEND lapply [ "lapply" constr(c) ] -> [ Tactics.cut_and_apply c ] END + +TACTIC EXTEND transitivity + [ "transitivity" constr(c) ] -> [ Tactics.intros_transitivity (Some c) ] +END diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 22ea274cb7..3b1cdecfb6 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -554,7 +554,6 @@ let rec intern_atomic lf ist x = (* Equivalence relations *) | TacSymmetry idopt -> TacSymmetry (clause_app (intern_hyp_location ist) idopt) - | TacTransitivity c -> TacTransitivity (Option.map (intern_constr ist) c) (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index a992c52ce1..12547e704d 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -1772,12 +1772,6 @@ and interp_atomic ist tac = let cl = interp_clause ist env c in Tactics.intros_symmetry cl end - | TacTransitivity c -> - begin match c with - | None -> Tactics.intros_transitivity None - | Some c -> - (new_interp_constr ist c) (fun c -> Tactics.intros_transitivity (Some c)) - end (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 4d0b595690..1b15fa8e18 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -195,7 +195,6 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Equivalence relations *) | TacSymmetry _ as x -> x - | TacTransitivity c -> TacTransitivity (Option.map (subst_glob_constr subst) c) (* Equality and inversion *) | TacRewrite (ev,l,cl,by) -> |