diff options
| author |  Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-22 16:31:58 +0200 |
|---|---|---|
| committer | Hugo Herbelin <Hugo.Herbelin@inria.fr> | 2014-06-28 18:52:26 +0200 |
| commit | 820dd1fa1c5d701c5f9af6e456b066d97a0d0499 (patch) | |
| tree | 09c01b7df330fe74046fd1a4cc90d55bb8bd7373 /pretyping/unification.mli | |
| parent | c41674da8b027de204d43831ca09a44bd1156c1f (diff) | |
Made the subterm finding function make_abstraction independent of the
proof engine. Moved it to unification.ml.
Diffstat (limited to 'pretyping/unification.mli')
| -rw-r--r-- | pretyping/unification.mli | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/pretyping/unification.mli b/pretyping/unification.mli index 3f93d817d..de8eecc27 100644 --- a/pretyping/unification.mli +++ b/pretyping/unification.mli @@ -53,6 +53,22 @@ val w_unify_meta_types : env -> ?flags:unify_flags -> evar_map -> evar_map val w_coerce_to_type : env -> evar_map -> constr -> types -> types -> evar_map * constr +(* Looking for subterms in contexts at some occurrences, possibly with pattern*) + +type abstraction_request = +| AbstractPattern of Names.Name.t * (evar_map * constr) * Locus.clause * bool * Pretyping.inference_flags +| AbstractExact of Names.Name.t * constr * types option * Locus.clause * bool + +val finish_evar_resolution : ?flags:Pretyping.inference_flags -> + env -> Evd.evar_map -> open_constr -> Evd.evar_universe_context * constr + +type abstraction_result = + Names.Id.t * Context.named_declaration list * Names.Id.t option * + constr * (Evd.evar_universe_context * constr) + +val make_abstraction : env -> Evd.evar_map -> constr -> + abstraction_request -> abstraction_result + (*i This should be in another module i*) (** [abstract_list_all env evd t c l] |