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/unification.mli | 54 +++++++++++++++++++++++++----------------------
 1 file changed, 29 insertions(+), 25 deletions(-)

(limited to 'pretyping/unification.mli')

diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index 0ad882a9..16ce5c93 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -1,12 +1,15 @@
 (************************************************************************)
-(*  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 Term
+open Constr
+open EConstr
 open Environ
 open Evd
 
@@ -44,7 +47,7 @@ val elim_no_delta_flags : unit -> unify_flags
 
 val is_keyed_unification : unit -> bool
 
-(** The "unique" unification fonction *)
+(** The "unique" unification function *)
 val w_unify :
   env -> evar_map -> conv_pb -> ?flags:unify_flags -> constr -> constr -> evar_map
 
@@ -71,18 +74,18 @@ exception PatternNotFound
 type prefix_of_inductive_support_flag = bool
 
 type abstraction_request =
-| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * pending_constr * Locus.clause * bool
+| AbstractPattern of prefix_of_inductive_support_flag * (types -> bool) * Names.Name.t * (evar_map * constr) * Locus.clause * bool
 | AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool
 
 val finish_evar_resolution : ?flags:Pretyping.inference_flags ->
-  env -> 'r Sigma.t -> pending_constr -> (constr, 'r) Sigma.sigma
+  env -> evar_map -> (evar_map * constr) -> evar_map * constr
 
 type 'r abstraction_result =
   Names.Id.t * named_context_val *
-    Context.Named.Declaration.t list * Names.Id.t option *
-    types * (constr, 'r) Sigma.sigma option
+    named_declaration list * Names.Id.t option *
+    types * (evar_map * constr) option
 
-val make_abstraction : env -> 'r Sigma.t -> constr ->
+val make_abstraction : env -> evar_map -> constr ->
   abstraction_request -> 'r abstraction_result
 
 val pose_all_metas_as_evars : env -> evar_map -> constr -> evar_map * constr
@@ -97,28 +100,29 @@ val abstract_list_all :
 
 (* For tracing *)
 
-val w_merge : env -> bool -> core_unify_flags -> evar_map *
-  (metavariable * constr * (instance_constraint * instance_typing_status)) list *
-  (env * types pexistential * types) list -> evar_map
+type metabinding = (metavariable * constr * (instance_constraint * instance_typing_status))
+
+type subst0 =
+  (evar_map *
+    metabinding list *
+      (Environ.env * existential * t) list)
+
+val w_merge : env -> bool -> core_unify_flags -> subst0 -> evar_map
 
 val unify_0 :            Environ.env ->
            Evd.evar_map ->
            Evd.conv_pb ->
            core_unify_flags ->
-           Term.types ->
-           Term.types ->
-           Evd.evar_map * Evd.metabinding list *
-           (Environ.env * Term.types Term.pexistential * Term.constr) list
+           types ->
+           types ->
+           subst0
 
 val unify_0_with_initial_metas : 
-           Evd.evar_map * Evd.metabinding list *
-           (Environ.env * Term.types Term.pexistential * Term.constr) list ->
+           subst0 ->
            bool ->
            Environ.env ->
            Evd.conv_pb ->
            core_unify_flags ->
-           Term.types ->
-           Term.types ->
-           Evd.evar_map * Evd.metabinding list *
-           (Environ.env * Term.types Term.pexistential * Term.constr) list
-
+           types ->
+           types ->
+           subst0
-- 
cgit v1.2.3