From 943b5f9a9a90e856171f9dcb13ae56eaa8d87ef0 Mon Sep 17 00:00:00 2001 From: ppedrot Date: Tue, 29 Oct 2013 19:47:14 +0000 Subject: Do not generate useless argument arrays in whd_* functions. git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16954 85f007b7-540e-0410-9357-904b9bb8a0f7 --- interp/notation.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'interp/notation.ml') diff --git a/interp/notation.ml b/interp/notation.ml index 5fa6346f0..737687adc 100644 --- a/interp/notation.ml +++ b/interp/notation.ml @@ -558,7 +558,7 @@ let scope_class_compare sc1 sc2 = match sc1, sc2 with let scope_class_of_reference x = ScopeRef x let compute_scope_class t = - let t', _ = Reductionops.whd_betaiotazeta_stack Evd.empty t in + let t', _ = decompose_appvect (Reductionops.whd_betaiotazeta Evd.empty t) in match kind_of_term t' with | Var _ | Const _ | Ind _ -> ScopeRef (global_of_constr t') | Sort _ -> ScopeSort -- cgit v1.2.3