diff options
| author |  Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-21 20:04:58 +0200 |
|---|---|---|
| committer | Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-04-27 21:39:25 +0200 |
| commit | 02d2f34e5c84f0169e884c07054a6fbfef9f365c (patch) | |
| tree | 5e55f22c5b20dcf694c00741a69dae6f1d993267 /plugins/ltac/tacintern.ml | |
| parent | 95239fa33c5da60080833dabc3ced246680dfdf9 (diff) | |
Remove some unused values and types
Diffstat (limited to 'plugins/ltac/tacintern.ml')
| -rw-r--r-- | plugins/ltac/tacintern.ml | 6 |
1 files changed, 0 insertions, 6 deletions
diff --git a/plugins/ltac/tacintern.ml b/plugins/ltac/tacintern.ml index 3f83f104e..75227def0 100644 --- a/plugins/ltac/tacintern.ml +++ b/plugins/ltac/tacintern.ml @@ -118,12 +118,6 @@ let intern_constr_reference strict ist = function GRef (loc,locate_global_with_alias lqid,None), if strict then None else Some (CRef (r,None)) -let intern_move_location ist = function - | MoveAfter id -> MoveAfter (intern_hyp ist id) - | MoveBefore id -> MoveBefore (intern_hyp ist id) - | MoveFirst -> MoveFirst - | MoveLast -> MoveLast - (* Internalize an isolated reference in position of tactic *) let intern_isolated_global_tactic_reference r = |