diff options
| author |  ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:56:25 +0000 |
|---|---|---|
| committer | ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-12-14 15:56:25 +0000 |
| commit | 67f5c70a480c95cfb819fc68439781b5e5e95794 (patch) | |
| tree | 67b88843ba54b4aefc7f604e18e3a71ec7202fd3 /kernel/reduction.ml | |
| parent | cc03a5f82efa451b6827af9a9b42cee356ed4f8a (diff) | |
Modulification of identifier
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@16071 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'kernel/reduction.ml')
| -rw-r--r-- | kernel/reduction.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/kernel/reduction.ml b/kernel/reduction.ml index fb6ffd2d1..9aa70c9eb 100644 --- a/kernel/reduction.ml +++ b/kernel/reduction.ml @@ -26,7 +26,7 @@ open Esubst let unfold_reference ((ids, csts), infos) k = match k with - | VarKey id when not (Idpred.mem id ids) -> None + | VarKey id when not (Id.Pred.mem id ids) -> None | ConstKey cst when not (Cpred.mem cst csts) -> None | _ -> unfold_reference infos k @@ -446,7 +446,7 @@ let trans_conv_cmp ?(l2r=false) conv reds = trans_fconv reds conv l2r (fun _->No let trans_conv ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv reds CONV l2r evars let trans_conv_leq ?(l2r=false) ?(evars=fun _->None) reds = trans_fconv reds CUMUL l2r evars -let fconv = trans_fconv (Idpred.full, Cpred.full) +let fconv = trans_fconv (Id.Pred.full, Cpred.full) let conv_cmp ?(l2r=false) cv_pb = fconv cv_pb l2r (fun _->None) let conv ?(l2r=false) ?(evars=fun _->None) = fconv CONV l2r evars |