From 7dcd829d1439a5f2d435234b72e0f595bf64eeff Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Wed, 15 Apr 2020 15:54:08 +0200
Subject: Minor cut elimination in the code of constrintern.ml.

---
 interp/constrintern.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/interp/constrintern.ml b/interp/constrintern.ml
index 032a752fe0..409e46864e 100644
--- a/interp/constrintern.ml
+++ b/interp/constrintern.ml
@@ -1731,9 +1731,9 @@ let drop_notations_pattern (test_kind_top,test_kind_inner) genv env pat =
     | CPatNotation (_,ntn,fullargs,extrargs) ->
       let ntn,(terms,termlists) = contract_curly_brackets_pat ntn fullargs in
       let ((ids',c),df) = Notation.interp_notation ?loc ntn scopes in
-      let (terms,termlists) = split_by_type_pat ?loc ids' (terms,termlists) in
+      let subst = split_by_type_pat ?loc ids' (terms,termlists) in
       Dumpglob.dump_notation_location (patntn_loc ?loc fullargs ntn) ntn df;
-      in_not test_kind loc scopes (terms,termlists) extrargs c
+      in_not test_kind loc scopes subst extrargs c
     | CPatDelimiters (key, e) ->
       in_pat test_kind (None,find_delimiters_scope ?loc key::snd scopes) e
     | CPatPrim p ->
-- 
cgit v1.2.3