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. --- plugins/ltac/tacinterp.ml | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'plugins/ltac/tacinterp.ml') diff --git a/plugins/ltac/tacinterp.ml b/plugins/ltac/tacinterp.ml index 2a1e2b682..8fa95ffb0 100644 --- a/plugins/ltac/tacinterp.ml +++ b/plugins/ltac/tacinterp.ml @@ -679,8 +679,8 @@ let interp_typed_pattern ist env sigma (_,c,_) = (* Interprets a constr expression *) let interp_constr_in_compound_list inj_fun dest_fun interp_fun ist env sigma l = let try_expand_ltac_var sigma x = - try match dest_fun x with - | { CAst.v = GVar id }, _ -> + try match DAst.get (fst (dest_fun x)) with + | GVar id -> let v = Id.Map.find id ist.lfun in sigma, List.map inj_fun (coerce_to_constr_list env v) | _ -> @@ -1043,7 +1043,7 @@ let interp_destruction_arg ist gl arg = if Tactics.is_quantified_hypothesis id gl then keep,ElimOnIdent (loc,id) else - let c = (CAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in + let c = (DAst.make ?loc @@ GVar id,Some (CAst.make @@ CRef (Ident (loc,id),None))) in let f env sigma = let (sigma,c) = interp_open_constr ist env sigma c in (sigma, (c,NoBindings)) -- cgit v1.2.3