fix a bug in factoring

uwplse · Feb 26, 2018 · f20c67b · f20c67b
1 parent a75afde
commit f20c67b
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/plugin/src/core/components/factoring/factoring.ml b/plugin/src/core/components/factoring/factoring.ml
@@ -90,7 +90,7 @@ let rec find_path (env : env) (trm : types) : factors =
          let assume_arg i a = apply_assumption (Array.get paths i) a in
          let args_assumed = Array.mapi assume_arg args in
 	 try
-           let t = unshift (infer_type env_arg arg) in
+           let t = unshift (reduce_term env_arg (infer_type env_arg arg)) in
 	   (assume env Anonymous t, mkApp (f, args_assumed)) :: path
 	 with _ ->
 	   []