Imported Upstream version 8.6

1 files changed, 0 insertions, 234 deletions

diff --git a/kernel/closure.mli b/kernel/closure.mli
deleted file mode 100644
index 4b8f8722..00000000
--- a/kernel/closure.mli
+++ /dev/null
@@ -1,234 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-open Names
-open Term
-open Environ
-open Esubst
-
-(** Flags for profiling reductions. *)
-val stats : bool ref
-val share : bool ref
-
-val with_stats: 'a Lazy.t -> 'a
-
-(** {6 ... } *)
-(** Delta implies all consts (both global (= by
-  [kernel_name]) and local (= by [Rel] or [Var])), all evars, and letin's.
-  Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of
-  a LetIn expression is Letin reduction *)
-
-
-
-val all_opaque      : transparent_state
-val all_transparent : transparent_state
-
-val is_transparent_variable : transparent_state -> variable -> bool
-val is_transparent_constant : transparent_state -> constant -> bool
-
-(** Sets of reduction kinds. *)
-module type RedFlagsSig = sig
-  type reds
-  type red_kind
-
-  (** {7 The different kinds of reduction } *)
-
-  val fBETA : red_kind
-  val fDELTA : red_kind
-  val fETA : red_kind
-  (** This flag is never used by the kernel reduction but pretyping does *)
-  val fIOTA : red_kind
-  val fZETA : red_kind
-  val fCONST : constant -> red_kind
-  val fVAR : Id.t -> red_kind
-
-  (** No reduction at all *)
-  val no_red : reds
-
-  (** Adds a reduction kind to a set *)
-  val red_add : reds -> red_kind -> reds
-
-  (** Removes a reduction kind to a set *)
-  val red_sub : reds -> red_kind -> reds
-
-  (** Adds a reduction kind to a set *)
-  val red_add_transparent : reds -> transparent_state -> reds
-
-  (** Build a reduction set from scratch = iter [red_add] on [no_red] *)
-  val mkflags : red_kind list -> reds
-
-  (** Tests if a reduction kind is set *)
-  val red_set : reds -> red_kind -> bool
-    
-  (** This tests if the projection is in unfolded state already or
-      is unfodable due to delta. *)
-  val red_projection : reds -> projection -> bool
-end
-
-module RedFlags : RedFlagsSig
-open RedFlags
-
-val beta               : reds
-val betaiota           : reds
-val betadeltaiota      : reds
-val betaiotazeta       : reds
-val betadeltaiotanolet : reds
-
-val unfold_side_red : reds
-val unfold_red : evaluable_global_reference -> reds
-
-(***********************************************************************)
-type table_key = constant puniverses tableKey
-
-type 'a infos_cache
-type 'a infos = { 
-  i_flags : reds;
-  i_cache : 'a infos_cache }
-
-val ref_value_cache: 'a infos -> table_key -> 'a option
-val create: ('a infos -> constr -> 'a) -> reds -> env ->
-  (existential -> constr option) -> 'a infos
-val evar_value : 'a infos_cache -> existential -> constr option
-
-val info_env : 'a infos -> env
-val info_flags: 'a infos -> reds
-
-(***********************************************************************
-  s Lazy reduction. *)
-
-(** [fconstr] is the type of frozen constr *)
-
-type fconstr
-
-(** [fconstr] can be accessed by using the function [fterm_of] and by
-   matching on type [fterm] *)
-
-type fterm =
-  | FRel of int
-  | FAtom of constr (** Metas and Sorts *)
-  | FCast of fconstr * cast_kind * fconstr
-  | FFlex of table_key
-  | FInd of inductive puniverses
-  | FConstruct of constructor puniverses
-  | FApp of fconstr * fconstr array
-  | FProj of projection * fconstr
-  | FFix of fixpoint * fconstr subs
-  | FCoFix of cofixpoint * fconstr subs
-  | FCase of case_info * fconstr * fconstr * fconstr array
-  | FCaseT of case_info * constr * fconstr * constr array * fconstr subs (* predicate and branches are closures *)
-  | FLambda of int * (Name.t * constr) list * constr * fconstr subs
-  | FProd of Name.t * fconstr * fconstr
-  | FLetIn of Name.t * fconstr * fconstr * constr * fconstr subs
-  | FEvar of existential * fconstr subs
-  | FLIFT of int * fconstr
-  | FCLOS of constr * fconstr subs
-  | FLOCKED
-
-(***********************************************************************
-  s A [stack] is a context of arguments, arguments are pushed by
-   [append_stack] one array at a time but popped with [decomp_stack]
-   one by one *)
-
-type stack_member =
-  | Zapp of fconstr array
-  | Zcase of case_info * fconstr * fconstr array
-  | ZcaseT of case_info * constr * constr array * fconstr subs
-  | Zproj of int * int * constant
-  | Zfix of fconstr * stack
-  | Zshift of int
-  | Zupdate of fconstr
-
-and stack = stack_member list
-
-val empty_stack : stack
-val append_stack : fconstr array -> stack -> stack
-
-val decomp_stack : stack -> (fconstr * stack) option
-val array_of_stack : stack -> fconstr array
-val stack_assign : stack -> int -> fconstr -> stack
-val stack_args_size : stack -> int
-val stack_tail : int -> stack -> stack
-val stack_nth : stack -> int -> fconstr
-val zip_term : (fconstr -> constr) -> constr -> stack -> constr
-val eta_expand_stack : stack -> stack
-
-(** To lazy reduce a constr, create a [clos_infos] with
-   [create_clos_infos], inject the term to reduce with [inject]; then use
-   a reduction function *)
-
-val inject : constr -> fconstr
-
-(** mk_atom: prevents a term from being evaluated *)
-val mk_atom : constr -> fconstr
-
-val fterm_of : fconstr -> fterm
-val term_of_fconstr : fconstr -> constr
-val destFLambda :
-  (fconstr subs -> constr -> fconstr) -> fconstr -> Name.t * fconstr * fconstr
-
-(** Global and local constant cache *)
-type clos_infos = fconstr infos
-val create_clos_infos :
-  ?evars:(existential->constr option) -> reds -> env -> clos_infos
-val oracle_of_infos : clos_infos -> Conv_oracle.oracle
-
-val env_of_infos : clos_infos -> env
-
-val infos_with_reds : clos_infos -> reds -> clos_infos
-
-(** Reduction function *)
-
-(** [norm_val] is for strong normalization *)
-val norm_val : clos_infos -> fconstr -> constr
-
-(** [whd_val] is for weak head normalization *)
-val whd_val : clos_infos -> fconstr -> constr
-
-(** [whd_stack] performs weak head normalization in a given stack. It
-   stops whenever a reduction is blocked. *)
-val whd_stack :
-  clos_infos -> fconstr -> stack -> fconstr * stack
-
-(** [eta_expand_ind_stack env ind c s t] computes stacks correspoding 
-    to the conversion of the eta expansion of t, considered as an inhabitant 
-    of ind, and the Constructor c of this inductive type applied to arguments
-    s.
-    @assumes [t] is a rigid term, and not a constructor. [ind] is the inductive
-    of the constructor term [c] 
-    @raises Not_found if the inductive is not a primitive record, or if the 
-    constructor is partially applied.
- *)
-val eta_expand_ind_stack : env -> inductive -> fconstr -> stack -> 
-   (fconstr * stack) -> stack * stack
-
-(** Conversion auxiliary functions to do step by step normalisation *)
-
-(** [unfold_reference] unfolds references in a [fconstr] *)
-val unfold_reference : clos_infos -> table_key -> fconstr option
-
-val eq_table_key : table_key -> table_key -> bool
-
-(***********************************************************************
-  i This is for lazy debug *)
-
-val lift_fconstr      : int -> fconstr -> fconstr
-val lift_fconstr_vect : int -> fconstr array -> fconstr array
-
-val mk_clos      : fconstr subs -> constr -> fconstr
-val mk_clos_vect : fconstr subs -> constr array -> fconstr array
-val mk_clos_deep :
-  (fconstr subs -> constr -> fconstr) ->
-   fconstr subs -> constr -> fconstr
-
-val kni: clos_infos -> fconstr -> stack -> fconstr * stack
-val knr: clos_infos -> fconstr -> stack -> fconstr * stack
-val kl : clos_infos -> fconstr -> constr
-
-val to_constr : (lift -> fconstr -> constr) -> lift -> fconstr -> constr
-
-(** End of cbn debug section i*)