]> matita.cs.unibo.it Git - fireball-separation.git/commitdiff
Fix: it was always stepping on one non-existing argument
authoracondolu <andrea.condoluci@unibo.it>
Mon, 11 Jun 2018 09:53:21 +0000 (11:53 +0200)
committeracondolu <andrea.condoluci@unibo.it>
Mon, 11 Jun 2018 09:53:21 +0000 (11:53 +0200)
ocaml/simple.ml

index 13400b7f8cb84cb94c36c65daae5bd3a3a0dcf42..7c372cbe7191c71c0fe8749b543cda39d1794501 100644 (file)
@@ -266,7 +266,7 @@ let find_eta_difference p t =
  let divargs = args_of_inert p.div in\r
  let conargs = args_of_inert t in\r
  let rec range i j =\r
-  if j = -1 then [] else i :: range (i+1) (j-1) in\r
+  if j = 0 then [] else i :: range (i+1) (j-1) in\r
  let rec aux k divargs conargs =\r
   match divargs,conargs with\r
      [],conargs -> range k (List.length conargs)\r