diff options
| author | herbelin | 2004-01-29 15:20:33 +0000 |
|---|---|---|
| committer | herbelin | 2004-01-29 15:20:33 +0000 |
| commit | d204288bf38e3cecc2a60f07ce0b1bc3681f56da (patch) | |
| tree | 0e7d9c6463083fc14819061a908c5536e795ecce /pretyping/evarutil.mli | |
| parent | 29c33c1143635d89b82048835082c133439fffbd (diff) | |
Reparation d'une rupture (en presence de types implicites) de l'invariant que les variables liees sont toujours nommees
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@5268 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'pretyping/evarutil.mli')
| -rw-r--r-- | pretyping/evarutil.mli | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/pretyping/evarutil.mli b/pretyping/evarutil.mli index 4747bf065e..812f3e9342 100644 --- a/pretyping/evarutil.mli +++ b/pretyping/evarutil.mli @@ -89,7 +89,7 @@ val mk_valcon : constr -> val_constraint val split_tycon : Rawterm.loc -> env -> evar_defs -> type_constraint -> - type_constraint * type_constraint + name * type_constraint * type_constraint val valcon_of_tycon : type_constraint -> val_constraint |