diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-25 13:36:45 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2011-10-25 13:36:45 +0000 |
| commit | 1ae71d6b88f79ceedad611bbf1a9128800a275b0 (patch) | |
| tree | 41dd18c54ade03a9bcb184617bbd7a8e9e5c1209 /pretyping/evarutil.mli | |
| parent | b31a26f32f2600ba88653086a871dc1fafce4d4d (diff) | |
Continuing r1492 (useless changes were inadvertantly committed)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14593 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 10 |
1 files changed, 0 insertions, 10 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 54fc07265..365276853 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -62,16 +62,6 @@ type conv_fun = val evar_define : conv_fun -> ?choose:bool -> env -> evar_map -> existential -> constr -> evar_map -val materialize_evar_from_sign : - (env -> evar_map -> existential -> constr -> evar_map) -> - env -> evar_map -> int -> - named_context_val -> bool list -> constr list -> types -> - evar_map * constr * existential - -val solve_evar_evar : - (env -> evar_map -> existential -> constr -> evar_map) -> - env -> evar_map -> existential -> existential -> evar_map - (** {6 Evars/Metas switching...} *) (** [evars_to_metas] generates new metavariables for each non dependent |