diff options
| author | herbelin | 2007-09-26 20:59:34 +0000 |
|---|---|---|
| committer | herbelin | 2007-09-26 20:59:34 +0000 |
| commit | 142a857315eeccd54ef37792d66458d95a4dd78f (patch) | |
| tree | 7d00c27aa5f833beaf8ce85e080c06e5ce4fff0e /pretyping/evarutil.mli | |
| parent | 5f4a8ef2cd2a8ad965366530bef9e793337b023b (diff) | |
Complément aux commits 10124 et 10125 sur l'inférence de type (correction
de plusieurs bugs d'indice, de List.rev, d'oubli d'application de
whd_evar + code plus concis pour l'argument optionnel "filter").
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@10145 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index a3c3267e12..36b674fe5a 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -34,10 +34,10 @@ val new_untyped_evar : unit -> existential_key (***********************************************************) (* Creating a fresh evar given their type and context *) val new_evar : - evar_defs -> env -> ?src:loc * hole_kind -> ?filter:bool list option -> types -> evar_defs * constr + evar_defs -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> evar_defs * constr (* the same with side-effects *) val e_new_evar : - evar_defs ref -> env -> ?src:loc * hole_kind -> ?filter:bool list option -> types -> constr + evar_defs ref -> env -> ?src:loc * hole_kind -> ?filter:bool list -> types -> constr (* Create a fresh evar in a context different from its definition context: [new_evar_instance sign evd ty inst] creates a new evar of context @@ -46,7 +46,7 @@ val e_new_evar : of [inst] are typed in the occurrence context and their type (seen as a telescope) is [sign] *) val new_evar_instance : - named_context_val -> evar_defs -> types -> ?src:loc * hole_kind -> ?filter:bool list option -> constr list -> evar_defs * constr + named_context_val -> evar_defs -> types -> ?src:loc * hole_kind -> ?filter:bool list -> constr list -> evar_defs * constr (***********************************************************) (* Instantiate evars *) |