Merge remote-tracking branch 'origin/sail2' into c_fixes

1 files changed, 8 insertions, 8 deletions

diff --git a/src/pretty_print_lem.ml b/src/pretty_print_lem.ml
index c872d420..9897bb7c 100644
--- a/src/pretty_print_lem.ml
+++ b/src/pretty_print_lem.ml
@@ -334,14 +334,14 @@ let replace_typ_size ctxt env (Typ_aux (t,a)) =
        let mk_typ nexp = 
          Some (Typ_aux (Typ_app (id, [Typ_arg_aux (Typ_arg_nexp nexp,Parse_ast.Unknown);ord;typ']),a))
        in
-       match Type_check.solve env size with
-       | Some n -> mk_typ (nconstant n)
-       | None ->
-          let is_equal nexp =
-            prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
-          in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with
-          | nexp -> mk_typ nexp
-          | exception Not_found -> None
+       let is_equal nexp =
+         prove env (NC_aux (NC_equal (size,nexp),Parse_ast.Unknown))
+       in match List.find is_equal (NexpSet.elements ctxt.bound_nexps) with
+       | nexp -> mk_typ nexp
+       | exception Not_found ->
+          match Type_check.solve env size with
+          | Some n -> mk_typ (nconstant n)
+          | None -> None
      end
   | _ -> None