From 3ef7797ef6fc605dfafb32523261fe1b023aeecb Mon Sep 17 00:00:00 2001 From: Samuel Mimram Date: Fri, 28 Apr 2006 14:59:16 +0000 Subject: Imported Upstream version 8.0pl3+8.1alpha --- proofs/clenv.mli | 142 ------------------------------------------------------- 1 file changed, 142 deletions(-) delete mode 100644 proofs/clenv.mli (limited to 'proofs/clenv.mli') 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 *) -(* 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 -- cgit v1.2.3