diff options
| author |  Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-08-29 19:05:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2017-09-04 11:28:49 +0200 |
| commit | 1db568d3dc88d538f975377bb4d8d3eecd87872c (patch) | |
| tree | d8e35952cc8f6111875e664d8884dc2c7f908206 /plugins/ltac/tacinterp.ml | |
| parent | 3072bd9d080984833f5eb007bf15c6e9305619e3 (diff) | |
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.
Diffstat (limited to 'plugins/ltac/tacinterp.ml')
| -rw-r--r-- | plugins/ltac/tacinterp.ml | 6 |
1 files changed, 3 insertions, 3 deletions
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)) |