Imported Upstream version 8.0pl3+8.1alphaupstream/8.0pl3+8.1alpha

1 files changed, 0 insertions, 142 deletions

diff --git a/proofs/clenv.mli b/proofs/clenv.mli
deleted file mode 100644
index 737fbea3..00000000
--- a/proofs/clenv.mli
+++ /dev/null
@@ -1,142 +0,0 @@
-(************************************************************************)
-(*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
-(*   \VV/  **************************************************************)
-(*    //   *      This file is distributed under the terms of the       *)
-(*         *       GNU Lesser General Public License Version 2.1        *)
-(************************************************************************)
-
-(*i $Id: clenv.mli,v 1.32.2.2 2005/01/21 16:41:51 herbelin Exp $ i*)
-
-(*i*)
-open Util
-open Names
-open Term
-open Sign
-open Proof_type
-(*i*)
-
-(* [new_meta] is a generator of unique meta variables *)
-val new_meta : unit -> metavariable
-
-(* [exist_to_meta] generates new metavariables for each existential
-   and performs the replacement in the given constr *)
-val exist_to_meta :
-  Evd.evar_map -> Pretyping.open_constr -> (Termops.metamap * constr)
-
-(* The Type of Constructions clausale environments. *)
-
-module Metaset : Set.S with type elt = metavariable
-
-module Metamap : Map.S with type key = metavariable
-
-type 'a freelisted = {
-  rebus : 'a;
-  freemetas : Metaset.t }
-
-type clbinding = 
-  | Cltyp of constr freelisted
-  | Clval of constr freelisted * constr freelisted
-
-type 'a clausenv = {
-  templval : constr freelisted;
-  templtyp : constr freelisted;
-  namenv : identifier Metamap.t;
-  env : clbinding Metamap.t;
-  hook : 'a }
-
-type wc = named_context sigma (* for a better reading of the following *)
-
-(* [templval] is the template which we are trying to fill out.
- * [templtyp] is its type.
- * [namenv] is a mapping from metavar numbers to names, for
- *          use in instanciating metavars by name.
- * [env] is the mapping from metavar numbers to their types
- *       and values.
- * [hook] is the pointer to the current walking context, for
- *        integrating existential vars and metavars. *)
-
-val collect_metas : constr -> metavariable list
-val mk_clenv : 'a -> constr -> 'a clausenv
-val mk_clenv_from : 'a -> constr * constr -> 'a clausenv
-val mk_clenv_from_n : 'a -> int option -> constr * constr -> 'a clausenv
-val mk_clenv_rename_from : wc -> constr * constr -> wc clausenv
-val mk_clenv_rename_from_n : wc -> int option -> constr * constr -> wc clausenv
-val mk_clenv_hnf_constr_type_of : wc -> constr -> wc clausenv
-val mk_clenv_type_of : wc -> constr -> wc clausenv
-
-val subst_clenv : (substitution -> 'a -> 'a) -> 
-  substitution -> 'a clausenv -> 'a clausenv
-
-val connect_clenv : wc -> 'a clausenv -> wc clausenv
-(*i Was used in wcclausenv.ml
-val clenv_change_head : constr * constr -> 'a clausenv -> 'a clausenv
-i*)
-val clenv_assign : metavariable -> constr -> 'a clausenv -> 'a clausenv
-val clenv_instance_term : wc clausenv -> constr -> constr
-val clenv_pose : name * metavariable * constr -> 'a clausenv -> 'a clausenv
-val clenv_template : 'a clausenv -> constr freelisted
-val clenv_template_type : 'a clausenv -> constr freelisted
-val clenv_instance_type : wc clausenv -> metavariable -> constr
-val clenv_instance_template : wc clausenv -> constr
-val clenv_instance_template_type : wc clausenv -> constr
-val clenv_type_of : wc clausenv -> constr -> constr
-val clenv_fchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
-val clenv_bchain : metavariable -> 'a clausenv -> wc clausenv -> wc clausenv
-
-(* Unification with clenv *)
-type arg_bindings = (int * constr) list
-
-val unify_0 : 
-  Reductionops.conv_pb -> wc -> constr -> constr 
-    -> Termops.metamap * (constr * constr) list
-val clenv_unify : 
-  bool -> Reductionops.conv_pb -> constr -> constr ->
-  wc clausenv -> wc clausenv
-val clenv_match_args :
-  constr Rawterm.explicit_bindings -> wc clausenv -> wc clausenv
-val clenv_constrain_with_bindings : arg_bindings -> wc clausenv -> wc clausenv
-
-(* Bindings *)
-val clenv_independent : wc clausenv -> metavariable list
-val clenv_missing : 'a clausenv -> metavariable list
-val clenv_constrain_missing_args : (* Used in user contrib Lannion *)
-  constr list -> wc clausenv -> wc clausenv
-(*i
-val clenv_constrain_dep_args : constr list -> wc clausenv -> wc clausenv
-i*)
-val clenv_lookup_name : 'a clausenv -> identifier -> metavariable
-val clenv_unique_resolver : bool -> wc clausenv -> goal sigma -> wc clausenv
-
-val make_clenv_binding_apply :
-  wc -> int -> constr * constr -> types Rawterm.bindings -> wc clausenv
-val make_clenv_binding :
-  wc -> constr * constr -> types Rawterm.bindings -> wc clausenv
-
-(* Tactics *)
-val unify : constr -> tactic
-val clenv_refine : (wc -> tactic) -> wc clausenv -> tactic
-val res_pf      : (wc -> tactic) -> wc clausenv -> tactic
-val res_pf_cast : (wc -> tactic) -> wc clausenv -> tactic
-val elim_res_pf : (wc -> tactic) -> wc clausenv -> bool -> tactic
-val e_res_pf : (wc -> tactic) -> wc clausenv -> tactic
-val elim_res_pf_THEN_i : 
-  (wc -> tactic) -> wc clausenv -> (wc clausenv -> tactic array) -> tactic
-
-(* Pretty-print *)
-val pr_clenv : 'a clausenv -> Pp.std_ppcmds
-
-(* Exported for debugging *)
-val unify_to_subterm : 
-  wc clausenv -> constr * constr -> wc clausenv * constr
-val unify_to_subterm_list : 
-  bool -> wc clausenv -> constr list -> constr -> wc clausenv * constr list
-val clenv_typed_unify :
-  Reductionops.conv_pb -> constr -> constr -> wc clausenv -> wc clausenv
-
-(*i This should be in another module i*)
-
-(* [abstract_list_all env sigma t c l]                     *)
-(* abstracts the terms in l over c to get a term of type t *)
-val abstract_list_all :
-  Environ.env -> Evd.evar_map -> constr -> constr -> constr list -> constr