Dterm: admit formulas in let-in (fixes #19565)

c3fcec7b · Andrei Paskevich · Guillaume Melquiond · 7fdaad84 · c3fcec7b
Commit c3fcec7b authored Sep 25, 2015 by Andrei Paskevich Committed by Guillaume Melquiond Oct 13, 2015
--- a/src/core/dterm.ml
+++ b/src/core/dterm.ml
@@ -204,9 +204,7 @@ let denv_get denv n = Mstr.find_exn (UnboundVar n) n denv

 let denv_get_opt denv n = Mstr.find_opt n denv

-let dty_of_dterm dt = match dt.dt_dty with
-  | None -> Loc.error ?loc:dt.dt_loc TermExpected
-  | Some dty -> dty
+let dty_of_dterm dt = Opt.get_def dty_bool dt.dt_dty

 let denv_empty = Mstr.empty