From a4c7f8bd98be2a200489325ff7c5061cf80ab4f3 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <gareuselesinge@debian.org>
Date: Tue, 27 Dec 2016 16:53:30 +0100
Subject: Imported Upstream version 8.6

---
 pretyping/cases.mli | 17 +++++++++--------
 1 file changed, 9 insertions(+), 8 deletions(-)

(limited to 'pretyping/cases.mli')

diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index ab00aa16..ee4148de 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -8,7 +8,6 @@
 
 open Names
 open Term
-open Context
 open Evd
 open Environ
 open Inductiveops
@@ -33,6 +32,8 @@ val error_wrong_numarg_constructor_loc : Loc.t -> env -> constructor -> int -> '
 
 val error_wrong_numarg_inductive_loc : Loc.t -> env -> inductive -> int -> 'a
 
+val irrefutable : env -> cases_pattern -> bool
+
 (** {6 Compilation primitive. } *)
 
 val compile_cases :
@@ -45,11 +46,11 @@ val compile_cases :
 val constr_of_pat : 
            Environ.env ->
            Evd.evar_map ref ->
-           rel_declaration list ->
+           Context.Rel.Declaration.t list ->
            Glob_term.cases_pattern ->
            Names.Id.t list ->
            Glob_term.cases_pattern *
-           (rel_declaration list * Term.constr *
+           (Context.Rel.Declaration.t list * Term.constr *
             (Term.types * Term.constr list) * Glob_term.cases_pattern) *
            Names.Id.t list
 
@@ -83,7 +84,7 @@ type tomatch_status =
   | Pushed of (bool*((constr * tomatch_type) * int list * Name.t))
   | Alias of (bool * (Name.t * constr * (constr * types)))
   | NonDepAlias
-  | Abstract of int * rel_declaration
+  | Abstract of int * Context.Rel.Declaration.t
 
 type tomatch_stack = tomatch_status list
 
@@ -113,11 +114,11 @@ 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) ->
+            Environ.env -> Evd.evar_map ref -> glob_constr -> Environ.unsafe_judgment) ->
            Environ.env ->
            Evd.evar_map ->
            (Term.types * tomatch_type) list ->
-           Context.rel_context list ->
+           Context.Rel.t list ->
            Constr.constr option ->
-           'a option -> (Evd.evar_map * Names.name list * Term.constr) list
-
+           glob_constr option ->
+           (Evd.evar_map * Names.name list * Term.constr) list
-- 
cgit v1.2.3