diff options
| author | Pierre-Marie Pédrot | 2018-07-25 15:56:49 +0200 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2018-07-25 15:56:49 +0200 |
| commit | 523de4f878293cf1d582bd70300b34d497e705b3 (patch) | |
| tree | 5037ac2e2fd60003d582d800466657df624b848f /pretyping/tacred.ml | |
| parent | 9b6ce4f1848c546d0d361aa1089fa2907ca4c9ad (diff) | |
| parent | cb219011534a8de24a01ddb007799133cdd2cb0e (diff) | |
Merge PR #7889: Cleanup reduction effects: they only work on constants.
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 599a0f8162..8911a2f343 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 |