diff options
Diffstat (limited to 'src/pretty_print_lem.ml')
| -rw-r--r-- | src/pretty_print_lem.ml | 16 |
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 |