diff options
| author | herbelin | 2002-04-11 14:21:11 +0000 |
|---|---|---|
| committer | herbelin | 2002-04-11 14:21:11 +0000 |
| commit | 38398456ebae7069569fe97f20796ebfb8aee8de (patch) | |
| tree | a0eac947f292d842ab042d58cc666fdaed439456 /pretyping/evarutil.mli | |
| parent | 94b5ebb389a321376540b6437fc1fcceaf26e65d (diff) | |
Deuxième passe sur la localisation des messages d'erreurs sur les evars non définies
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@2633 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index f75bd31b1f..4fce79be28 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -65,8 +65,8 @@ val solve_simple_eqn : (env -> evar_defs -> conv_pb -> constr -> constr -> bool) -> env -> evar_defs -> conv_pb * existential * constr -> bool -val define_evar_as_arrow : evar_map -> existential -> evar_map * types -val define_evar_as_sort : evar_map -> existential -> evar_map * sorts +val define_evar_as_arrow : evar_defs -> existential -> types +val define_evar_as_sort : evar_defs -> existential -> sorts (* Value/Type constraints *) |