From 884b6cc6c12bd557085cdaa4972d593684c9cc1a Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 24 Oct 2014 17:38:59 +0200 Subject: Change reduction_of_red_expr to return an e_reduction_function returning an updated evar_map, as pattern is working up to universe equalities that must be kept. Straightforward adaptation of the code depending on this. --- plugins/funind/recdef.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'plugins/funind') diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index ca9f995f1..0d254c9af 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -675,7 +675,7 @@ let mkDestructEq : (fun g2 -> change_in_concl None (fun env sigma -> - sigma, pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) Evd.empty (pf_concl g2)) g2); + pattern_occs [Locus.AllOccurrencesBut [1], expr] (pf_env g2) sigma (pf_concl g2)) g2); Proofview.V82.of_tactic (simplest_case expr)]), to_revert -- cgit v1.2.3