From 9043add656177eeac1491a73d2f3ab92bec0013c Mon Sep 17 00:00:00 2001
From: Benjamin Barenblat <bbaren@debian.org>
Date: Sat, 29 Dec 2018 14:31:27 -0500
Subject: Imported Upstream version 8.8.2

---
 pretyping/cases.mli | 68 ++++++++++++++++++++++++++++++-----------------------
 1 file changed, 38 insertions(+), 30 deletions(-)

(limited to 'pretyping/cases.mli')

diff --git a/pretyping/cases.mli b/pretyping/cases.mli
index ee4148de..04a34646 100644
--- a/pretyping/cases.mli
+++ b/pretyping/cases.mli
@@ -1,18 +1,22 @@
 (************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
+(*         *   The Coq Proof Assistant / The Coq Development Team       *)
+(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
+(* <O___,, *       (see CREDITS file for the list of authors)           *)
 (*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
+(*    //   *    This file is distributed under the terms of the         *)
+(*         *     GNU Lesser General Public License Version 2.1          *)
+(*         *     (see LICENSE file for the text of the license)         *)
 (************************************************************************)
 
 open Names
-open Term
+open Constr
 open Evd
 open Environ
+open EConstr
 open Inductiveops
 open Glob_term
-open Evarutil
+open Ltac_pretype
+open Evardefine
 
 (** {5 Compilation of pattern-matching } *)
 
@@ -28,43 +32,43 @@ type pattern_matching_error =
 
 exception PatternMatchingError of env * evar_map * pattern_matching_error
 
-val error_wrong_numarg_constructor_loc : Loc.t -> env -> constructor -> int -> 'a
+val error_wrong_numarg_constructor : ?loc:Loc.t -> env -> constructor -> int -> 'a
 
-val error_wrong_numarg_inductive_loc : Loc.t -> env -> inductive -> int -> 'a
+val error_wrong_numarg_inductive   : ?loc:Loc.t -> env -> inductive -> int -> 'a
 
 val irrefutable : env -> cases_pattern -> bool
 
 (** {6 Compilation primitive. } *)
 
 val compile_cases :
-  Loc.t -> case_style ->
-  (type_constraint -> env -> evar_map ref -> glob_constr -> unsafe_judgment) * evar_map ref ->
+  ?loc:Loc.t -> case_style ->
+  (type_constraint -> env -> evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) * evar_map ref ->
   type_constraint ->
-  env -> glob_constr option * tomatch_tuples * cases_clauses ->
+  env -> ltac_var_map -> glob_constr option * tomatch_tuples * cases_clauses ->
   unsafe_judgment
 
 val constr_of_pat : 
            Environ.env ->
            Evd.evar_map ref ->
-           Context.Rel.Declaration.t list ->
+           rel_context ->
            Glob_term.cases_pattern ->
-           Names.Id.t list ->
+           Names.Id.Set.t ->
            Glob_term.cases_pattern *
-           (Context.Rel.Declaration.t list * Term.constr *
-            (Term.types * Term.constr list) * Glob_term.cases_pattern) *
-           Names.Id.t list
+           (rel_context * constr *
+            (types * constr list) * Glob_term.cases_pattern) *
+           Names.Id.Set.t
 
 type 'a rhs =
     { rhs_env    : env;
-      rhs_vars   : Id.t list;
-      avoid_ids  : Id.t list;
+      rhs_vars   : Id.Set.t;
+      avoid_ids  : Id.Set.t;
       it         : 'a option}
 
 type 'a equation =
     { patterns     : cases_pattern list;
       rhs          : 'a rhs;
       alias_stack  : Name.t list;
-      eqn_loc      : Loc.t;
+      eqn_loc      : Loc.t option;
       used         : bool ref }
 
 type 'a matrix = 'a equation list
@@ -84,7 +88,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 * Context.Rel.Declaration.t
+  | Abstract of int * rel_declaration
 
 type tomatch_stack = tomatch_status list
 
@@ -100,25 +104,29 @@ and pattern_continuation =
 
 type 'a pattern_matching_problem =
     { env       : env;
+      lvar      : Ltac_pretype.ltac_var_map;
       evdref    : evar_map ref;
       pred      : constr;
       tomatch   : tomatch_stack;
       history   : pattern_continuation;
       mat       : 'a matrix;
-      caseloc   : Loc.t;
+      caseloc   : Loc.t option;
       casestyle : case_style;
       typing_function: type_constraint -> env -> evar_map ref -> 'a option -> unsafe_judgment }
 
 
-val compile : 'a pattern_matching_problem -> Environ.unsafe_judgment
+val compile : 'a pattern_matching_problem -> unsafe_judgment
 
-val prepare_predicate :            Loc.t ->
-           (Evarutil.type_constraint ->
-            Environ.env -> Evd.evar_map ref -> glob_constr -> Environ.unsafe_judgment) ->
+val prepare_predicate : ?loc:Loc.t ->
+           (type_constraint ->
+            Environ.env -> Evd.evar_map ref -> ltac_var_map -> glob_constr -> unsafe_judgment) ->
            Environ.env ->
            Evd.evar_map ->
-           (Term.types * tomatch_type) list ->
-           Context.Rel.t list ->
-           Constr.constr option ->
-           glob_constr option ->
-           (Evd.evar_map * Names.name list * Term.constr) list
+           Ltac_pretype.ltac_var_map ->
+           (types * tomatch_type) list ->
+           (rel_context * rel_context) list ->
+           constr option ->
+           glob_constr option -> (Evd.evar_map * Name.t list * constr) list
+
+val make_return_predicate_ltac_lvar : Evd.evar_map -> Name.t ->
+  Glob_term.glob_constr -> constr -> Ltac_pretype.ltac_var_map -> ltac_var_map
-- 
cgit v1.2.3