diff options
| author | Gaëtan Gilbert | 2018-06-21 15:07:56 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert | 2018-07-12 14:07:25 +0200 |
| commit | cb219011534a8de24a01ddb007799133cdd2cb0e (patch) | |
| tree | e754dd9853ef891c5daecfa6987881048f8952b1 /pretyping/tacred.ml | |
| parent | 31fce698ec8c3186dc6af49961e8572e81cab50b (diff) | |
Cleanup reduction effects: they only work on constants.
We only ever call `reduction_effect_hook` on constants, so there's no
point allowing it to be declared with globrefs. There is also no point
using a constr map instead of constant map.
(Technically there was a call of the effect hook on projections, but
that can never match a globref so it was useless)
Diffstat (limited to 'pretyping/tacred.ml')
| -rw-r--r-- | pretyping/tacred.ml | 6 |
1 files changed, 2 insertions, 4 deletions
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml index 40c4cfaa45..ac1859480d 100644 --- a/pretyping/tacred.ml +++ b/pretyping/tacred.ml @@ -539,7 +539,7 @@ let reduce_mind_case_use_function func env sigma mia = let match_eval_ref env sigma constr stack = match EConstr.kind sigma constr with | Const (sp, u) -> - reduction_effect_hook env sigma (EConstr.to_constr sigma constr) + reduction_effect_hook env sigma sp (lazy (EConstr.to_constr sigma (applist (constr,stack)))); if is_evaluable env (EvalConstRef sp) then Some (EvalConst sp, u) else None | Var id when is_evaluable env (EvalVarRef id) -> Some (EvalVar id, EInstance.empty) @@ -550,7 +550,7 @@ let match_eval_ref env sigma constr stack = let match_eval_ref_value env sigma constr stack = match EConstr.kind sigma constr with | Const (sp, u) -> - reduction_effect_hook env sigma (EConstr.to_constr sigma constr) + reduction_effect_hook env sigma sp (lazy (EConstr.to_constr sigma (applist (constr,stack)))); if is_evaluable env (EvalConstRef sp) then let u = EInstance.kind sigma u in @@ -558,8 +558,6 @@ let match_eval_ref_value env sigma constr stack = else None | Proj (p, c) when not (Projection.unfolded p) -> - reduction_effect_hook env sigma (EConstr.to_constr ~abort_on_undefined_evars:false sigma constr) - (lazy (EConstr.to_constr sigma (applist (constr,stack)))); if is_evaluable env (EvalConstRef (Projection.constant p)) then Some (mkProj (Projection.unfold p, c)) else None |