diff options
| author | herbelin | 2000-05-31 11:46:29 +0000 |
|---|---|---|
| committer | herbelin | 2000-05-31 11:46:29 +0000 |
| commit | 301d5af223390fa5c82da9ae9958f610493ba814 (patch) | |
| tree | 304f4b7b194ace4c6fac67af90a0bcdf3ff3537f /kernel/typeops.mli | |
| parent | aca8a6bbb4fa372cd3b27680eee642082d1c2ad5 (diff) | |
Nettoyage de Generic
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@482 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/typeops.mli')
| -rw-r--r-- | kernel/typeops.mli | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/typeops.mli b/kernel/typeops.mli index 7ab2404f8c..3d2074c977 100644 --- a/kernel/typeops.mli +++ b/kernel/typeops.mli @@ -67,8 +67,8 @@ val apply_rel_list : env -> 'a evar_map -> bool -> unsafe_judgment list -> unsafe_judgment -> unsafe_judgment * constraints -val check_fix : env -> 'a evar_map -> constr -> unit -val check_cofix : env -> 'a evar_map -> constr -> unit +val check_fix : env -> 'a evar_map -> fixpoint -> unit +val check_cofix : env -> 'a evar_map -> cofixpoint -> unit val control_only_guard : env -> 'a evar_map -> constr -> unit val type_fixpoint : env -> 'a evar_map -> name list -> typed_type array |