Merge pull request #3301 from mtzguido/fix_free

Syntax.Free: fix incomplete match
FStarLang · May 22, 2024 · 8ec46c7 · 8ec46c7
2 parents d839af4 + feba44c
commit 8ec46c7
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/ocaml/fstar-lib/generated/FStar_Syntax_Free.ml b/ocaml/fstar-lib/generated/FStar_Syntax_Free.ml
diff --git a/src/syntax/FStar.Syntax.Free.fst b/src/syntax/FStar.Syntax.Free.fst
@@ -175,7 +175,7 @@ let rec free_names_and_uvs' tm (use_cache:use_cache_t) : free_vars_and_fvars =
       | Tm_match {scrutinee=t; ret_opt=asc_opt; brs=pats; rc_opt} ->
         (match rc_opt with
          | Some { residual_typ = Some t } -> free_names_and_uvars t use_cache
-         | None -> no_free_vars) ++
+         | _ -> no_free_vars) ++
         begin
         pats |> List.fold_left (fun n (p, wopt, t) ->
             let n1 = match wopt with