Do not add proof obligation for subrange free constants

src/lustre/lustreAstNormalizer.ml

@@ -1194,19 +1194,19 @@ and normalize_node info map
   let gids7 = locals
     |> List.filter (function
       | A.NodeVarDecl (_, (_, id, _, _)) 
-      | A.NodeConstDecl (_, FreeConst (_, id, _)) 
       | A.NodeConstDecl (_, TypedConst (_, id, _, _)) -> 
         let ty = get_type_of_id info node_id id in
         Ctx.type_contains_subrange ctx ty || Ctx.type_contains_ref ctx ty
+      | A.NodeConstDecl (_, FreeConst _)
       | A.NodeConstDecl (_, UntypedConst _) -> false)
     |> List.fold_left (fun acc l -> match l with
       | A.NodeVarDecl (p, (_, id, _, _)) 
-      | A.NodeConstDecl (p, FreeConst (_, id, _)) 
       | A.NodeConstDecl (p, TypedConst (_, id, _, _)) ->  
         let ty = get_type_of_id info node_id id in
         let ty = AIC.inline_constants_of_lustre_type info.context ty in
         let gids = union acc (mk_fresh_subrange_constraint Local info p (Some node_id) id ty)
         in union gids (mk_fresh_refinement_type_constraint Local info p (A.Ident (p, id)) ty)
+      | A.NodeConstDecl (_, FreeConst _)
       | A.NodeConstDecl (_, UntypedConst _)-> assert false)
       (empty ())
   in