From 362e81735b07f96cb87e1203328592fc394beaad Mon Sep 17 00:00:00 2001
From: Matthieu Sozeau
Date: Tue, 17 Jun 2014 15:22:18 +0200
Subject: - Fix the de Bruijn problem in check_projection for good :) - Fix
 HoTT coq bug #80, implicit arguments with primitive projections were wrongly
 automatically infered.

---
 pretyping/cases.mli | 11 +++++++++++
 1 file changed, 11 insertions(+)

(limited to 'pretyping')

diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index 70fa945ff1..d875edd796 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -110,3 +110,14 @@ type 'a pattern_matching_problem =
 
 
 val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment
+
+val prepare_predicate :            Loc.t ->
+           (Evarutil.type_constraint ->
+            Environ.env -> Evd.evar_map ref -> 'a -> Environ.unsafe_judgment) ->
+           Evd.evar_map ->
+           Environ.env ->
+           (Term.types * tomatch_type) list ->
+           Context.rel_context list ->
+           Constr.constr option ->
+           'a option -> (Evd.evar_map * Names.name list * Term.constr) list
+
-- 
cgit v1.2.3