From 5eb53b5bc8d765ed75e965f43f1084e18efc8790 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sun, 27 Apr 2014 15:09:04 +0200
Subject: Adding a field ci_cstr_nargs to case_info and mind_consnrealargs to
 one_inductive_body so that when eta-expanding at "match" printing time we
 know if a let is part of the expected signature or part of the body.

This is an easy fix for bugs like #3293. Another fix could be to
enforce, as an invariant, or better syntactically, that
"match"/"Case"'s have the body of their branches expanded.
---
 lib/hashset.ml  | 1 +
 lib/hashset.mli | 1 +
 2 files changed, 2 insertions(+)

(limited to 'lib')

diff --git a/lib/hashset.ml b/lib/hashset.ml
index 8c40e55001..f8d4274dee 100644
--- a/lib/hashset.ml
+++ b/lib/hashset.ml
@@ -202,5 +202,6 @@ module Combine = struct
     let combine x y     = x * alpha + y
     let combine3 x y z   = combine x (combine y z)
     let combine4 x y z t = combine x (combine3 y z t)
+    let combine5 x y z t u = combine x (combine4 y z t u)
     let combinesmall x y = beta * x + y
 end
diff --git a/lib/hashset.mli b/lib/hashset.mli
index 2041b2ec20..2e5b814a79 100644
--- a/lib/hashset.mli
+++ b/lib/hashset.mli
@@ -43,4 +43,5 @@ module Combine : sig
   val combinesmall : int -> int -> int
   val combine3 : int -> int -> int -> int
   val combine4 : int -> int -> int -> int -> int
+  val combine5 : int -> int -> int -> int -> int -> int
 end
-- 
cgit v1.2.3