From 1db568d3dc88d538f975377bb4d8d3eecd87872c Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Tue, 29 Aug 2017 19:05:57 +0200 Subject: Making detyping potentially lazy. The internal detype function takes an additional arguments dictating whether it should be eager or lazy. We introduce a new type of delayed `DAst.t` AST nodes and use it for `glob_constr`. Such type, instead of only containing a value, it can contain a lazy computation too. We use a GADT to discriminate between both uses statically, so that no delayed terms ever happen to be marshalled (which would raise anomalies). We also fix a regression in the test-suite: Mixing laziness and effects is a well-known hell. Here, an exception that was raised for mere control purpose was delayed and raised at a later time as an anomaly. We make the offending function eager. --- interp/reserve.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/reserve.ml') diff --git a/interp/reserve.ml b/interp/reserve.ml index b05f05283..a1e5bd0ea 100644 --- a/interp/reserve.ml +++ b/interp/reserve.ml @@ -110,7 +110,7 @@ let revert_reserved_type t = let t = EConstr.Unsafe.to_constr t in let reserved = KeyMap.find (constr_key t) !reserve_revtable in let t = EConstr.of_constr t in - let t = Detyping.detype false [] (Global.env()) Evd.empty t in + let t = Detyping.detype Detyping.Now false [] (Global.env()) Evd.empty t in (* pedrot: if [Notation_ops.match_notation_constr] may raise [Failure _] then I've introduced a bug... *) let filter _ pat = -- cgit v1.2.3