diff options
| author | Pierre-Marie Pédrot | 2014-11-09 21:04:56 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2014-11-09 21:04:56 +0100 |
| commit | 2070c302639e841aae1558e8bc59cca6da099bdd (patch) | |
| tree | 991c54cf03e8e380714308a3ec154137b6cd7de4 /tactics | |
| parent | 90c398a7377ac4dbab5ed3add3cbbe9a1bea538a (diff) | |
Removing a unused boolean in the TacMove node of tacexpr AST.
Diffstat (limited to 'tactics')
| -rw-r--r-- | tactics/tacintern.ml | 4 | ||||
| -rw-r--r-- | tactics/tacinterp.ml | 4 | ||||
| -rw-r--r-- | tactics/tacsubst.ml | 2 |
3 files changed, 5 insertions, 5 deletions
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml index 9ca8da9d35..f3c7680b01 100644 --- a/tactics/tacintern.ml +++ b/tactics/tacintern.ml @@ -513,8 +513,8 @@ let rec intern_atomic lf ist x = (* Context management *) | TacClear (b,l) -> TacClear (b,List.map (intern_hyp ist) l) | TacClearBody l -> TacClearBody (List.map (intern_hyp ist) l) - | TacMove (dep,id1,id2) -> - TacMove (dep,intern_hyp ist id1,intern_move_location ist id2) + | TacMove (id1,id2) -> + TacMove (intern_hyp ist id1,intern_move_location ist id2) | TacRename l -> TacRename (List.map (fun (id1,id2) -> intern_hyp ist id1, diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml index b320e9bb16..feebfa40f6 100644 --- a/tactics/tacinterp.ml +++ b/tactics/tacinterp.ml @@ -2025,9 +2025,9 @@ and interp_atomic ist tac : unit Proofview.tactic = (TacClearBody l) (Tactics.clear_body l) end - | TacMove (dep,id1,id2) -> + | TacMove (id1,id2) -> Proofview.V82.tactic begin fun gl -> - Tactics.move_hyp dep (interp_hyp ist (pf_env gl) (project gl) id1) + Tactics.move_hyp true (interp_hyp ist (pf_env gl) (project gl) id1) (interp_move_location ist (pf_env gl) (project gl) id2) gl end diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml index 1eec2f257e..2f47b90002 100644 --- a/tactics/tacsubst.ml +++ b/tactics/tacsubst.ml @@ -185,7 +185,7 @@ let rec subst_atomic subst (t:glob_atomic_tactic_expr) = match t with (* Context management *) | TacClear _ as x -> x | TacClearBody l as x -> x - | TacMove (dep,id1,id2) as x -> x + | TacMove (id1,id2) as x -> x | TacRename l as x -> x (* Constructors *) |