diff options
| author | Pierre-Marie Pédrot | 2017-08-29 19:05:57 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2017-09-04 11:28:49 +0200 |
| commit | 1db568d3dc88d538f975377bb4d8d3eecd87872c (patch) | |
| tree | d8e35952cc8f6111875e664d8884dc2c7f908206 /plugins/ltac/g_rewrite.ml4 | |
| 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/g_rewrite.ml4')
| -rw-r--r-- | plugins/ltac/g_rewrite.ml4 | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/ltac/g_rewrite.ml4 b/plugins/ltac/g_rewrite.ml4 index c874f8d5a3..c22e683235 100644 --- a/plugins/ltac/g_rewrite.ml4 +++ b/plugins/ltac/g_rewrite.ml4 @@ -123,7 +123,7 @@ END let clsubstitute o c = Proofview.Goal.enter begin fun gl -> - let is_tac id = match fst (fst (snd c)) with { CAst.v = GVar id' } when Id.equal id' id -> true | _ -> false in + let is_tac id = match DAst.get (fst (fst (snd c))) with GVar id' when Id.equal id' id -> true | _ -> false in let hyps = Tacmach.New.pf_ids_of_hyps gl in Tacticals.New.tclMAP (fun cl -> |