diff options
| author |  filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-09-03 07:42:44 +0000 |
|---|---|---|
| committer | filliatr <filliatr@85f007b7-540e-0410-9357-904b9bb8a0f7> | 1999-09-03 07:42:44 +0000 |
| commit | 010a1652d7f0072b057235507c0efd5b7284574f (patch) | |
| tree | 8a85d489d96368230eca4e68add0e6fa953a5235 /kernel/typeops.ml | |
| parent | 7534d56bf9b4b5f23b1fe1df87288c2d7565853a (diff) | |
- environnements vides
- suppression du constructeur Implicit (et IsImplicit du coup)
- nettoyages divers
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@35 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/typeops.ml')
| -rw-r--r-- | kernel/typeops.ml | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/kernel/typeops.ml b/kernel/typeops.ml index 40f41d603..7e8161865 100644 --- a/kernel/typeops.ml +++ b/kernel/typeops.ml @@ -349,7 +349,6 @@ let type_of_sort c g = match c with | DOP0 (Sort (Type u)) -> let (uu,g') = super u g in mkType uu, g' | DOP0 (Sort (Prop _)) -> mkType prop_univ, g - | DOP0 (Implicit) -> mkImplicit, g | _ -> invalid_arg "type_of_sort" (* Type of a lambda-abstraction. *) @@ -743,6 +742,9 @@ let check_fix env = function (* Co-fixpoints. *) +let mind_nparams env i = + let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams + let check_guard_rec_meta env nbfix def deftype = let rec codomain_is_coind c = match whd_betadeltaiota env (strip_outer_cast c) with |