diff options
Diffstat (limited to 'tactics/stock.ml')
| -rw-r--r-- | tactics/stock.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/tactics/stock.ml b/tactics/stock.ml index b0fa6d0e81..ef0feec952 100644 --- a/tactics/stock.ml +++ b/tactics/stock.ml @@ -59,7 +59,7 @@ let mmk_ctr = ref 0 let new_mmk () = (incr mmk_ctr; !mmk_ctr) -let make_module_marker stock sl = +let make_module_marker sl = let sorted_sl = Sort.list (<) sl in try Bij.map !path_mark_bij sorted_sl |