1 files changed, 0 insertions, 148 deletions
diff --git a/pretyping/clenv.mli b/pretyping/clenv.mli
deleted file mode 100644
index 6fbb668b..00000000
--- a/pretyping/clenv.mli
+++ /dev/null
@@ -1,148 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2011     *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: clenv.mli 14641 2011-11-06 11:59:10Z herbelin $ i*)
-
-(*i*)
-open Util
-open Names
-open Term
-open Sign
-open Environ
-open Evd
-open Evarutil
-open Mod_subst
-open Rawterm
-open Unification
-(*i*)
-
-(***************************************************************)
-(* The Type of Constructions clausale environments. *)
-
-(* [env] is the typing context
- * [evd] is the mapping from metavar and evar numbers to their types
- *       and values.
- * [templval] is the template which we are trying to fill out.
- * [templtyp] is its type.
- *)
-type clausenv = {
-  env      : env;
-  evd      : evar_map;
-  templval : constr freelisted;
-  templtyp : constr freelisted }
-
-(* Substitution is not applied on templenv (because [subst_clenv] is
-   applied only on hints which typing env is overwritten by the
-   goal env) *)
-val subst_clenv : substitution -> clausenv -> clausenv
-
-(* subject of clenv (instantiated) *)
-val clenv_value     : clausenv -> constr
-(* type of clenv (instantiated) *)
-val clenv_type      : clausenv -> types
-(* substitute resolved metas *)
-val clenv_nf_meta   : clausenv -> constr -> constr
-(* type of a meta in clenv context *)
-val clenv_meta_type : clausenv -> metavariable -> types
-
-val mk_clenv_from : evar_info sigma -> constr * types -> clausenv
-val mk_clenv_from_n :
-  evar_info sigma -> int option -> constr * types -> clausenv
-val mk_clenv_type_of : evar_info sigma -> constr -> clausenv
-val mk_clenv_from_env : env -> evar_map -> int option -> constr * types -> clausenv
-
-(***************************************************************)
-(* linking of clenvs *)
-
-val connect_clenv : evar_info sigma -> clausenv -> clausenv
-val clenv_fchain :
-  ?allow_K:bool -> ?flags:unify_flags -> metavariable -> clausenv -> clausenv -> clausenv
-
-(***************************************************************)
-(* Unification with clenvs *)
-
-(* Unifies two terms in a clenv. The boolean is [allow_K] (see [Unification]) *)
-val clenv_unify :
-  bool -> ?flags:unify_flags -> conv_pb -> constr -> constr -> clausenv -> clausenv
-
-(* unifies the concl of the goal with the type of the clenv *)
-val clenv_unique_resolver :
-  bool -> ?flags:unify_flags -> clausenv -> evar_info sigma -> clausenv
-
-(* same as above ([allow_K=false]) but replaces remaining metas
-   with fresh evars if [evars_flag] is [true] *)
-val evar_clenv_unique_resolver :
-  bool -> ?flags:unify_flags -> clausenv -> evar_info sigma -> clausenv
-
-val clenv_dependent : bool -> clausenv -> metavariable list
-
-val clenv_pose_metas_as_evars : clausenv -> metavariable list -> clausenv
-
-(***************************************************************)
-(* Bindings *)
-
-type arg_bindings = constr explicit_bindings
-
-(* bindings where the key is the position in the template of the
-   clenv (dependent or not). Positions can be negative meaning to
-   start from the rightmost argument of the template. *)
-val clenv_independent : clausenv -> metavariable list
-val clenv_missing : clausenv -> metavariable list
-
-(** for the purpose of inversion tactics *)
-exception NoSuchBinding
-val clenv_constrain_last_binding : constr -> clausenv -> clausenv
-
-(* defines metas corresponding to the name of the bindings *)
-val clenv_match_args : arg_bindings -> clausenv -> clausenv
-
-val clenv_unify_meta_types : ?flags:unify_flags -> clausenv -> clausenv
-
-(* start with a clenv to refine with a given term with bindings *)
-
-(* the arity of the lemma is fixed *)
-(* the optional int tells how many prods of the lemma have to be used *)
-(* use all of them if None *)
-val make_clenv_binding_apply :
-  evar_info sigma -> int option -> constr * constr -> constr bindings ->
-   clausenv
-val make_clenv_binding_env_apply :
-  env -> evar_map -> int option -> constr * constr -> constr bindings ->
-   clausenv
-val make_clenv_binding :
-  evar_info sigma -> constr * constr -> constr bindings -> clausenv
-
-(* [clenv_environments sigma n t] returns [sigma',lmeta,ccl] where
-   [lmetas] is a list of metas to be applied to a proof of [t] so that
-   it produces the unification pattern [ccl]; [sigma'] is [sigma]
-   extended with [lmetas]; if [n] is defined, it limits the size of
-   the list even if [ccl] is still a product; otherwise, it stops when
-   [ccl] is not a product; example: if [t] is [forall x y, x=y -> y=x]
-   and [n] is [None], then [lmetas] is [Meta n1;Meta n2;Meta n3] and
-   [ccl] is [Meta n1=Meta n2]; if [n] is [Some 1], [lmetas] is [Meta n1]
-   and [ccl] is [forall y, Meta n1=y -> y=Meta n1] *)
-val clenv_environments :
- evar_map -> int option -> types -> evar_map * constr list * types
-
-(* [clenv_environments_evars env sigma n t] does the same but returns
-   a list of Evar's defined in [env] and extends [sigma] accordingly *)
-val clenv_environments_evars :
- env -> evar_map -> int option -> types -> evar_map * constr list * types
-
-(* [clenv_conv_leq env sigma t c n] looks for c1...cn s.t. [t <= c c1...cn] *)
-val clenv_conv_leq :
- env -> evar_map -> types -> constr -> int -> constr list
-
-(* if the clause is a product, add an extra meta for this product *)
-exception NotExtensibleClause
-val clenv_push_prod : clausenv -> clausenv
-
-(***************************************************************)
-(* Pretty-print *)
-val pr_clenv : clausenv -> Pp.std_ppcmds
-