diff options
| author | ppedrot | 2013-10-29 19:47:14 +0000 |
|---|---|---|
| committer | ppedrot | 2013-10-29 19:47:14 +0000 |
| commit | 943b5f9a9a90e856171f9dcb13ae56eaa8d87ef0 (patch) | |
| tree | 366dd6d33017f7f00f99ede753585be989f5a9ce /interp/notation.ml | |
| parent | b8098068f29a58a478efa719c51271d09f66a9d8 (diff) | |
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
Diffstat (limited to 'interp/notation.ml')
| -rw-r--r-- | interp/notation.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/interp/notation.ml b/interp/notation.ml index 5fa6346f03..737687adc3 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 |