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

---
 plugins/funind/indfun_common.mli | 65 +++++++++++++++++++++++-----------------
 1 file changed, 38 insertions(+), 27 deletions(-)

(limited to 'plugins/funind/indfun_common.mli')

diff --git a/plugins/funind/indfun_common.mli b/plugins/funind/indfun_common.mli
index e5c756f5..5cc7163a 100644
--- a/plugins/funind/indfun_common.mli
+++ b/plugins/funind/indfun_common.mli
@@ -1,5 +1,4 @@
 open Names
-open Pp
 
 (*
    The mk_?_id function build different name w.r.t. a function
@@ -11,7 +10,7 @@ val mk_complete_id : Id.t -> Id.t
 val mk_equation_id : Id.t -> Id.t
 
 
-val msgnl : std_ppcmds -> unit
+val msgnl : Pp.t -> unit
 
 val fresh_id : Id.t list -> string -> Id.t
 val fresh_name : Id.t list -> string -> Name.t
@@ -22,9 +21,9 @@ val array_get_start : 'a array -> 'a array
 val id_of_name : Name.t -> Id.t
 
 val locate_ind : Libnames.reference -> inductive
-val locate_constant : Libnames.reference -> constant
+val locate_constant : Libnames.reference -> Constant.t
 val locate_with_msg :
-  Pp.std_ppcmds -> (Libnames.reference -> 'a) ->
+  Pp.t -> (Libnames.reference -> 'a) ->
   Libnames.reference -> 'a
 
 val filter_map : ('a -> bool) -> ('a -> 'b) -> 'a list -> 'b list
@@ -34,17 +33,17 @@ val list_add_set_eq :
   ('a -> 'a -> bool) -> 'a -> 'a list -> 'a list
 
 val chop_rlambda_n : int -> Glob_term.glob_constr ->
-  (Name.t*Glob_term.glob_constr*bool) list * Glob_term.glob_constr
+  (Name.t*Glob_term.glob_constr*Glob_term.glob_constr option) list * Glob_term.glob_constr
 
 val chop_rprod_n : int -> Glob_term.glob_constr ->
   (Name.t*Glob_term.glob_constr) list * Glob_term.glob_constr
 
-val def_of_const : Term.constr -> Term.constr
-val eq : Term.constr Lazy.t
-val refl_equal : Term.constr Lazy.t
+val def_of_const : Constr.t -> Constr.t
+val eq : EConstr.constr Lazy.t
+val refl_equal : EConstr.constr Lazy.t
 val const_of_id: Id.t ->  Globnames.global_reference(* constantyes *)
-val jmeq : unit -> Term.constr
-val jmeq_refl : unit -> Term.constr
+val jmeq : unit -> EConstr.constr
+val jmeq_refl : unit -> EConstr.constr
 
 val save : bool -> Id.t -> Safe_typing.private_constants Entries.definition_entry  -> Decl_kinds.goal_kind ->
   unit Lemmas.declaration_hook CEphemeron.key -> unit
@@ -69,28 +68,28 @@ val with_full_print : ('a -> 'b) -> 'a -> 'b
 
 type function_info =
     {
-      function_constant : constant;
+      function_constant : Constant.t;
       graph_ind : inductive;
-      equation_lemma : constant option;
-      correctness_lemma : constant option;
-      completeness_lemma : constant option;
-      rect_lemma : constant option;
-      rec_lemma : constant option;
-      prop_lemma : constant option;
+      equation_lemma : Constant.t option;
+      correctness_lemma : Constant.t option;
+      completeness_lemma : Constant.t option;
+      rect_lemma : Constant.t option;
+      rec_lemma : Constant.t option;
+      prop_lemma : Constant.t option;
       is_general : bool;
     }
 
-val find_Function_infos : constant -> function_info
+val find_Function_infos : Constant.t -> function_info
 val find_Function_of_graph : inductive -> function_info
 (* WARNING: To be used just after the graph definition !!! *)
-val add_Function : bool -> constant -> unit
+val add_Function : bool -> Constant.t -> unit
 
 val update_Function : function_info -> unit
 
 
 (** debugging *)
-val pr_info : function_info -> Pp.std_ppcmds
-val pr_table : unit -> Pp.std_ppcmds
+val pr_info : function_info -> Pp.t
+val pr_table : unit -> Pp.t
 
 
 (* val function_debug : bool ref  *)
@@ -104,13 +103,25 @@ exception ToShow of exn
 
 val is_strict_tcc : unit -> bool
 
-val h_intros: Names.Id.t list -> Proof_type.tactic
+val h_intros: Names.Id.t list -> Tacmach.tactic
 val h_id :  Names.Id.t
 val hrec_id :  Names.Id.t
-val acc_inv_id :  Term.constr Util.delayed
+val acc_inv_id :  EConstr.constr Util.delayed
 val ltof_ref : Globnames.global_reference Util.delayed
-val well_founded_ltof : Term.constr Util.delayed
-val acc_rel : Term.constr Util.delayed
-val well_founded : Term.constr Util.delayed
+val well_founded_ltof : EConstr.constr Util.delayed
+val acc_rel : EConstr.constr Util.delayed
+val well_founded : EConstr.constr Util.delayed
 val evaluable_of_global_reference : Globnames.global_reference -> Names.evaluable_global_reference
-val list_rewrite : bool -> (Term.constr*bool) list -> Proof_type.tactic
+val list_rewrite : bool -> (EConstr.constr*bool) list -> Tacmach.tactic
+
+val decompose_lam_n : Evd.evar_map -> int -> EConstr.t ->
+  (Names.Name.t * EConstr.t) list * EConstr.t
+val compose_lam : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
+val compose_prod : (Names.Name.t * EConstr.t) list -> EConstr.t -> EConstr.t
+
+type tcc_lemma_value =
+  | Undefined
+  | Value of Constr.t
+  | Not_needed
+
+val funind_purify : ('a -> 'b) -> ('a -> 'b)
-- 
cgit v1.2.3