diff options
| author | ppedrot | 2012-11-08 17:11:59 +0000 |
|---|---|---|
| committer | ppedrot | 2012-11-08 17:11:59 +0000 |
| commit | b0b1710ba631f3a3a3faad6e955ef703c67cb967 (patch) | |
| tree | 9d35a8681cda8fa2dc968535371739684425d673 /kernel/indtypes.ml | |
| parent | bafb198e539998a4a64b2045a7e85125890f196e (diff) | |
Monomorphized a lot of equalities over OCaml integers, thanks to
the new Int module. Only the most obvious were removed, so there
are a lot more in the wild.
This may sound heavyweight, but it has two advantages:
1. Monomorphization is explicit, hence we do not miss particular
optimizations of equality when doing it carelessly with the generic
equality.
2. When we have removed all the generic equalities on integers, we
will be able to write something like "let (=) = ()" to retrieve all
its other uses (mostly faulty) spread throughout the code, statically.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15957 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/indtypes.ml')
| -rw-r--r-- | kernel/indtypes.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/kernel/indtypes.ml b/kernel/indtypes.ml index 1c12c9e244..6b993604d1 100644 --- a/kernel/indtypes.ml +++ b/kernel/indtypes.ml @@ -349,7 +349,7 @@ let check_correct_par (env,n,ntypes,_) hyps l largs = recursive parameters *) let compute_rec_par (env,n,_,_) hyps nmr largs = -if nmr = 0 then 0 else +if Int.equal nmr 0 then 0 else (* start from 0, hyps will be in reverse order *) let (lpar,_) = List.chop nmr largs in let rec find k index = @@ -371,7 +371,7 @@ let lambda_implicit_lift n a = (* This removes global parameters of the inductive types in lc (for nested inductive types only ) *) let abstract_mind_lc env ntyps npars lc = - if npars = 0 then + if Int.equal npars 0 then lc else let make_abs = @@ -411,7 +411,7 @@ let rec ienv_decompose_prod (env,_,_,_ as ienv) n c = ienv_decompose_prod ienv' (n-1) b | _ -> assert false -let array_min nmr a = if nmr = 0 then 0 else +let array_min nmr a = if Int.equal nmr 0 then 0 else Array.fold_left (fun k (nmri,_) -> min k nmri) nmr a (* The recursive function that checks positivity and builds the list @@ -620,7 +620,7 @@ let build_inductive env env_ar params isrecord isfinite inds nmr recargs cst = let nconst, nblock = ref 0, ref 0 in let transf num = let arity = List.length (dest_subterms recarg).(num) in - if arity = 0 then + if Int.equal arity 0 then let p = (!nconst, 0) in incr nconst; p else |