diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-08 17:11:59 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-11-08 17:11:59 +0000 |
| commit | b0b1710ba631f3a3a3faad6e955ef703c67cb967 (patch) | |
| tree | 9d35a8681cda8fa2dc968535371739684425d673 /tactics/btermdn.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 'tactics/btermdn.ml')
| -rw-r--r-- | tactics/btermdn.ml | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/tactics/btermdn.ml b/tactics/btermdn.ml index e8cde2967..819c76807 100644 --- a/tactics/btermdn.ml +++ b/tactics/btermdn.ml @@ -81,7 +81,7 @@ struct | _ -> Dn.Nothing let bounded_constr_pat_discr_st st (t,depth) = - if depth = 0 then + if Int.equal depth 0 then None else match Term_dn.constr_pat_discr_st st t with @@ -89,7 +89,7 @@ struct | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) let bounded_constr_val_discr_st st (t,depth) = - if depth = 0 then + if Int.equal depth 0 then Dn.Nothing else match constr_val_discr_st st t with @@ -98,7 +98,7 @@ struct | Dn.Everything -> Dn.Everything let bounded_constr_pat_discr (t,depth) = - if depth = 0 then + if Int.equal depth 0 then None else match Term_dn.constr_pat_discr t with @@ -106,7 +106,7 @@ struct | Some (c,l) -> Some(c,List.map (fun c -> (c,depth-1)) l) let bounded_constr_val_discr (t,depth) = - if depth = 0 then + if Int.equal depth 0 then Dn.Nothing else match constr_val_discr t with |