From 441bace297a4c31e5003cec93e46e6a47fa684d3 Mon Sep 17 00:00:00 2001
From: Gaëtan Gilbert
Date: Wed, 17 Feb 2021 13:56:27 +0100
Subject: Use make_case_or_project in auto_ind_decl

Towards #5154 (but insufficient)
---
 engine/eConstr.mli | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'engine')

diff --git a/engine/eConstr.mli b/engine/eConstr.mli
index 0d038e9a67..162d189136 100644
--- a/engine/eConstr.mli
+++ b/engine/eConstr.mli
@@ -365,6 +365,8 @@ val to_rel_decl : Evd.evar_map -> (t, types) Context.Rel.Declaration.pt -> (Cons
 
 val of_case_invert : Constr.case_invert -> case_invert
 
+val of_constr_array : Constr.t array -> t array
+
 (** {5 Unsafe operations} *)
 
 module Unsafe :
-- 
cgit v1.2.3